---

Step * of Lemma M-bind_wf

∀[Mnd:Monad]. (M-bind(Mnd) ∈ ⋂T,S:Type.  ((M-map(Mnd) T) ⟶ (T ⟶ (M-map(Mnd) S)) ⟶ (M-map(Mnd) S)))
BY
{ ((UnivCD THENA Auto)
   THEN Unfold `monad` 1
   THEN D 1
   THEN D 2
   THEN D 3
   THEN Unfolds ``M-bind M-map`` 0
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  Unfold  `monad`  1
  THEN  D  1
  THEN  D  2
  THEN  D  3
  THEN  Unfolds  ``M-bind  M-map``  0
  THEN  Reduce  0
  THEN  Auto)

---

Home Index