---

Step * of Lemma M-return_wf

∀[Mnd:Monad]. (M-return(Mnd) ∈ ⋂T:Type. (T ⟶ (M-map(Mnd) T)))
BY
{ ((UnivCD THENA Auto) THEN RepeatFor 3 (D -1) THEN RepUR ``M-return M-map`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[Mnd:Monad].  (M-return(Mnd)  \mmember{}  \mcap{}T:Type.  (T  {}\mrightarrow{}  (M-map(Mnd)  T)))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  RepeatFor  3  (D  -1)  THEN  RepUR  ``M-return  M-map``  0  THEN  Auto)

---

Home Index