---

Step * 1 1 1 of Lemma comp_id_mon_wf


1. T : Type
⊢ ∀[x,y,z:T ⟶ T].  ((x o (y o z)) = ((x o y) o z) ∈ (T ⟶ T))
BY
{ UnivCD THENA Auto }

1
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)

---

Latex:

---

Latex:

1.  T  :  Type
\mvdash{}  \mforall{}[x,y,z:T  {}\mrightarrow{}  T].    ((x  o  (y  o  z))  =  ((x  o  y)  o  z))


By

---

Latex:
UnivCD  THENA  Auto

---

Home Index