Step * 1 1 1 1 of Lemma perm_igrp_wf


T:Type. ∀[x,y,z:Perm(T)].  (x 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