Step
*
1
3
1
of Lemma
perm_igrp_wf
∀T:Type. ∀[x:Perm(T)]. ((x O inv_perm(x) = id_perm() ∈ Perm(T)) ∧ (inv_perm(x) O x = id_perm() ∈ Perm(T)))
BY
{ (Auto THEN BLemma `perm_inverse` THEN Auto) }
Latex:
Latex:
\mforall{}T:Type. \mforall{}[x:Perm(T)]. ((x O inv\_perm(x) = id\_perm()) \mwedge{} (inv\_perm(x) O x = id\_perm()))
By
Latex:
(Auto THEN BLemma `perm\_inverse` THEN Auto)
Home
Index