---

Step * of Lemma perm_igrp_wf

∀[T:Type]. (perm_igrp(T) ∈ IGroup)
BY
{ ((Unfold `perm_igrp` 0 THEN D 0) THENA Auto) }

1
1. T : Type
⊢ mk_igrp(Perm(T);λp,q. p O q;id_perm();λp.inv_perm(p)) ∈ IGroup

---

Latex:

---

Latex:
\mforall{}[T:Type].  (perm\_igrp(T)  \mmember{}  IGroup)


By

---

Latex:
((Unfold  `perm\_igrp`  0  THEN  D  0)  THENA  Auto)

---

Home Index