pub fn initial_algebra_ty() -> Expr
InitialAlgebra : (Type → Type) → Type → Prop
Lambek’s lemma: the initial algebra of F is a fixed point F(Mu F) ≅ Mu F.