---

Step * of Lemma comp_assoc

∀[A,B,C,D:Type]. ∀[f:A ⟶ B]. ∀[g:B ⟶ C]. ∀[h:C ⟶ D].  ((h o (g o f)) = ((h o g) o f) ∈ (A ⟶ D))
BY
{ ((UnivCD THENM (Unfold `compose` 0 THEN Reduce 0)) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A,B,C,D:Type].  \mforall{}[f:A  {}\mrightarrow{}  B].  \mforall{}[g:B  {}\mrightarrow{}  C].  \mforall{}[h:C  {}\mrightarrow{}  D].    ((h  o  (g  o  f))  =  ((h  o  g)  o  f))


By

---

Latex:
((UnivCD  THENM  (Unfold  `compose`  0  THEN  Reduce  0))  THEN  Auto)

---

Home Index