---

Step * 1 of Lemma mk_igrp_wf


1. T : Type
2. op : T ⟶ T ⟶ T
3. id : T
4. inv : T ⟶ T
5. Assoc(T;op)
6. Ident(T;op;id)
7. Inverse(T;op;id;inv)
⊢ <T, λx,y. tt, λx,y. tt, op, id, inv> ∈ IGroup
BY
{ MemTypeCD THENA Auto }

1
1. T : Type
2. op : T ⟶ T ⟶ T
3. id : T
4. inv : T ⟶ T
5. Assoc(T;op)
6. Ident(T;op;id)
7. Inverse(T;op;id;inv)
⊢ <T, λx,y. tt, λx,y. tt, op, id, inv> ∈ IMonoid

---

Latex:

---

Latex:

1.  T  :  Type
2.  op  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  T
3.  id  :  T
4.  inv  :  T  {}\mrightarrow{}  T
5.  Assoc(T;op)
6.  Ident(T;op;id)
7.  Inverse(T;op;id;inv)
\mvdash{}  <T,  \mlambda{}x,y.  tt,  \mlambda{}x,y.  tt,  op,  id,  inv>  \mmember{}  IGroup


By

---

Latex:
MemTypeCD  THENA  Auto

---

Home Index