---

Step * 2 3 1 of Lemma monad-from_wf


1. Mnd : Monad
2. λx,z. (M-bind(Mnd) z (λx.x)) ∈ A:Type ⟶ (M-map(Mnd) (M-map(Mnd) A)) ⟶ (M-map(Mnd) A)
3. X : Type
4. x : M-map(Mnd) X
⊢ (M-bind(Mnd) x (λx@0.(M-return(Mnd) x@0))) = x ∈ (M-map(Mnd) X)
BY
{ ((InstLemma `M-rightunit` [⌜Mnd⌝;⌜X⌝;⌜x⌝]⋅ THENA Auto) THEN NthHypEq (-1) THEN EqCDA) }

1
.....subterm..... T:t
2:n
1. Mnd : Monad
2. λx,z. (M-bind(Mnd) z (λx.x)) ∈ A:Type ⟶ (M-map(Mnd) (M-map(Mnd) A)) ⟶ (M-map(Mnd) A)
3. X : Type
4. x : M-map(Mnd) X
5. (M-bind(Mnd) x M-return(Mnd)) = x ∈ (M-map(Mnd) X)
⊢ (M-bind(Mnd) x (λx@0.(M-return(Mnd) x@0))) = (M-bind(Mnd) x M-return(Mnd)) ∈ (M-map(Mnd) X)

---

Latex:

---

Latex:

1.  Mnd  :  Monad
2.  \mlambda{}x,z.  (M-bind(Mnd)  z  (\mlambda{}x.x))  \mmember{}  A:Type  {}\mrightarrow{}  (M-map(Mnd)  (M-map(Mnd)  A))  {}\mrightarrow{}  (M-map(Mnd)  A)
3.  X  :  Type
4.  x  :  M-map(Mnd)  X
\mvdash{}  (M-bind(Mnd)  x  (\mlambda{}x@0.(M-return(Mnd)  x@0)))  =  x


By

---

Latex:
((InstLemma  `M-rightunit`  [\mkleeneopen{}Mnd\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  NthHypEq  (-1)  THEN  EqCDA)

---

Home Index