---

Step * 1 of Lemma perm_igrp_wf


1. T : Type
⊢ mk_igrp(Perm(T);λp,q. p O q;id_perm();λp.inv_perm(p)) ∈ IGroup
BY
{ (MemCD THEN Auto) }

1
1. T : Type
⊢ Assoc(Perm(T);λp,q. p O q)

2
1. T : Type
⊢ Ident(Perm(T);λp,q. p O q;id_perm())

3
1. T : Type
⊢ Inverse(Perm(T);λp,q. p O q;id_perm();λp.inv_perm(p))

---

Latex:

---

Latex:

1.  T  :  Type
\mvdash{}  mk\_igrp(Perm(T);\mlambda{}p,q.  p  O  q;id\_perm();\mlambda{}p.inv\_perm(p))  \mmember{}  IGroup


By

---

Latex:
(MemCD  THEN  Auto)

---

Home Index