---

Step * 1 1 1 1 of Lemma comp_id_mon_wf


1. T : Type
2. x : T ⟶ T
3. y : T ⟶ T
4. z : T ⟶ T
⊢ (x o (y o z)) = ((x o y) o z) ∈ (T ⟶ T)
BY
{ BackThruLemma `comp_assoc` 
THEN Auto }

---

Latex:

---

Latex:

1.  T  :  Type
2.  x  :  T  {}\mrightarrow{}  T
3.  y  :  T  {}\mrightarrow{}  T
4.  z  :  T  {}\mrightarrow{}  T
\mvdash{}  (x  o  (y  o  z))  =  ((x  o  y)  o  z)


By

---

Latex:
BackThruLemma  `comp\_assoc` 
THEN  Auto

---

Home Index