---

Step * of Lemma perm_mon_assoc

∀[T:Type]. ∀[a,b,c:Perm(T)].  (a O b O c = a O b O c ∈ Perm(T))
BY
{ (ProveSpecializedLemma `mon_assoc` 1 [parm{i}; perm_igrp(T)] (AbReduceC)) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[a,b,c:Perm(T)].    (a  O  b  O  c  =  a  O  b  O  c)


By

---

Latex:
(ProveSpecializedLemma  `mon\_assoc`  1  [parm\{i\};  perm\_igrp(T)]  (AbReduceC))

---

Home Index