---

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