---

Step * 1 1 of Lemma comp_id_mon_wf


1. T : Type
⊢ Assoc(T ⟶ T;λf,g. (f o g))
BY
{ UnfoldTopAb 0  
THEN AbReduce 0 
 }

1
1. T : Type
⊢ ∀[x,y,z:T ⟶ T].  ((x o (y o z)) = ((x o y) o z) ∈ (T ⟶ T))

---

Latex:

---

Latex:

1.  T  :  Type
\mvdash{}  Assoc(T  {}\mrightarrow{}  T;\mlambda{}f,g.  (f  o  g))


By

---

Latex:
UnfoldTopAb  0   
THEN  AbReduce  0 

---

Home Index