---

Step * of Lemma mtype_wf

∀[Mn:Monad]. (mtype(Mn) ∈ Type ⟶ Type)
BY
{ (Auto THEN D -1 THEN RepUR ``mtype`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[Mn:Monad].  (mtype(Mn)  \mmember{}  Type  {}\mrightarrow{}  Type)


By

---

Latex:
(Auto  THEN  D  -1  THEN  RepUR  ``mtype``  0  THEN  Auto)

---

Home Index