Step
*
1
1
1
1
of Lemma
perm_igrp_wf
∀T:Type. ∀[x,y,z:Perm(T)].  (x O y O z = x O y O z ∈ Perm(T))
BY
{ TACTIC:(Auto THEN BLemma `perm_assoc`  THEN Auto) }
Latex:
Latex:
\mforall{}T:Type.  \mforall{}[x,y,z:Perm(T)].    (x  O  y  O  z  =  x  O  y  O  z)
By
Latex:
TACTIC:(Auto  THEN  BLemma  `perm\_assoc`    THEN  Auto)
Home
Index