---

Step * 1 of Lemma comp_id_mon_wf


1. T : Type
⊢ <T ⟶ T, λx,y. tt, λx,y. tt, λf,g. (f o g), Id, λx.x> ∈ IMonoid
BY
{ BackThruLemma `mk_imon` THEN Auto }

1
1. T : Type
⊢ Assoc(T ⟶ T;λf,g. (f o g))

2
1. T : Type
⊢ Ident(T ⟶ T;λf,g. (f o g);Id)

---

Latex:

---

Latex:

1.  T  :  Type
\mvdash{}  <T  {}\mrightarrow{}  T,  \mlambda{}x,y.  tt,  \mlambda{}x,y.  tt,  \mlambda{}f,g.  (f  o  g),  Id,  \mlambda{}x.x>  \mmember{}  IMonoid


By

---

Latex:
BackThruLemma  `mk\_imon`  THEN  Auto

---

Home Index