---

Step * of Lemma comp_id_mon_wf

∀[T:Type]. ((<o,Id> monoid on T) ∈ IMonoid)
BY
{ Unfold `comp_id_mon` 0  
THEN UnivCD THENA Auto }

1
1. T : Type
⊢ <T ⟶ T, λx,y. tt, λx,y. tt, λf,g. (f o g), Id, λx.x> ∈ IMonoid

---

Latex:

---

Latex:
\mforall{}[T:Type].  ((<o,Id>  monoid  on  T)  \mmember{}  IMonoid)


By

---

Latex:
Unfold  `comp\_id\_mon`  0   
THEN  UnivCD  THENA  Auto

---

Home Index