---

Step * of Lemma perm_grp_inv_inv

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

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[a:Perm(T)].    (inv\_perm(inv\_perm(a))  =  a)


By

---

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

---

Home Index