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