---

Step * 1 3 of Lemma perm_igrp_wf


1. T : Type
⊢ Inverse(Perm(T);λp,q. p O q;id_perm();λp.inv_perm(p))
BY
{ ((Unfold `inverse` 0 THEN AbReduce 0) THEN MoveToConcl 1) }

1
∀T:Type. ∀[x:Perm(T)]. ((x O inv_perm(x) = id_perm() ∈ Perm(T)) ∧ (inv_perm(x) O x = id_perm() ∈ Perm(T)))

---

Latex:

---

Latex:

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


By

---

Latex:
((Unfold  `inverse`  0  THEN  AbReduce  0)  THEN  MoveToConcl  1)

---

Home Index