---

Step * 1 of Lemma M-associative


1. M : Type ⟶ Type
2. return : ⋂T:Type. (T ⟶ (M T))
3. bind : ⋂T,S:Type.  ((M T) ⟶ (T ⟶ (M S)) ⟶ (M S))
4. leftunit : ∀[T,S:Type]. ∀[x:T]. ∀[f:T ⟶ (M S)].  ((bind (return x) f) = (f x) ∈ (M S))
5. rightunit : ∀[T:Type]. ∀[m:M T].  ((bind m return) = m ∈ (M T))
6. M5 : ∀[T,S,U:Type]. ∀[m:M T]. ∀[f:T ⟶ (M S)]. ∀[g:S ⟶ (M U)].
          ((bind (bind m f) g) = (bind m (λx.(bind (f x) g))) ∈ (M U))
7. T : Type
8. S : Type
9. U : Type
10. m : M-map(<M, return, bind, leftunit, rightunit, M5>) T
11. f : T ⟶ (M-map(<M, return, bind, leftunit, rightunit, M5>) S)
12. g : S ⟶ (M-map(<M, return, bind, leftunit, rightunit, M5>) U)
⊢ (bind (bind m f) g) = (bind m (λx.(bind (f x) g))) ∈ (M U)
BY
{ (AllHyps (\i. Try(Unfold `M-map` i THEN Reduce i)) THEN BackThruSomeHyp) }

---

Latex:

---

Latex:

1.  M  :  Type  {}\mrightarrow{}  Type
2.  return  :  \mcap{}T:Type.  (T  {}\mrightarrow{}  (M  T))
3.  bind  :  \mcap{}T,S:Type.    ((M  T)  {}\mrightarrow{}  (T  {}\mrightarrow{}  (M  S))  {}\mrightarrow{}  (M  S))
4.  leftunit  :  \mforall{}[T,S:Type].  \mforall{}[x:T].  \mforall{}[f:T  {}\mrightarrow{}  (M  S)].    ((bind  (return  x)  f)  =  (f  x))
5.  rightunit  :  \mforall{}[T:Type].  \mforall{}[m:M  T].    ((bind  m  return)  =  m)
6.  M5  :  \mforall{}[T,S,U:Type].  \mforall{}[m:M  T].  \mforall{}[f:T  {}\mrightarrow{}  (M  S)].  \mforall{}[g:S  {}\mrightarrow{}  (M  U)].
                    ((bind  (bind  m  f)  g)  =  (bind  m  (\mlambda{}x.(bind  (f  x)  g))))
7.  T  :  Type
8.  S  :  Type
9.  U  :  Type
10.  m  :  M-map(<M,  return,  bind,  leftunit,  rightunit,  M5>)  T
11.  f  :  T  {}\mrightarrow{}  (M-map(<M,  return,  bind,  leftunit,  rightunit,  M5>)  S)
12.  g  :  S  {}\mrightarrow{}  (M-map(<M,  return,  bind,  leftunit,  rightunit,  M5>)  U)
\mvdash{}  (bind  (bind  m  f)  g)  =  (bind  m  (\mlambda{}x.(bind  (f  x)  g)))


By

---

Latex:
(AllHyps  (\mbackslash{}i.  Try(Unfold  `M-map`  i  THEN  Reduce  i))  THEN  BackThruSomeHyp)

---

Home Index