---

Step * of Lemma perm_grp_inv_id

∀T:Type. (inv_perm(id_perm()) = id_perm() ∈ Perm(T))
BY
{ (ProveSpecializedLemma `grp_inv_id` 1 [parm{i}; perm_igrp(T)] (AbReduceC)) }

---

Latex:

---

Latex:
\mforall{}T:Type.  (inv\_perm(id\_perm())  =  id\_perm())


By

---

Latex:
(ProveSpecializedLemma  `grp\_inv\_id`  1  [parm\{i\};  perm\_igrp(T)]  (AbReduceC))

---

Home Index