---

Step * of Lemma parallel-class-com

∀[T,Info:Type]. ∀[X,Y:EClass(T)].  (X || Y = Y || X ∈ EClass(T))
BY
{ (Auto
   THEN RepUR ``parallel-class eclass-compose2 eclass`` 0
   THEN RepeatFor 2 ((EqCD THENA Auto))
   THEN BLemma `bag-append-comm`
   THEN Auto) }

---

Latex:


\mforall{}[T,Info:Type].  \mforall{}[X,Y:EClass(T)].    (X  ||  Y  =  Y  ||  X)


By

(Auto
  THEN  RepUR  ``parallel-class  eclass-compose2  eclass``  0
  THEN  RepeatFor  2  ((EqCD  THENA  Auto))
  THEN  BLemma  `bag-append-comm`
  THEN  Auto)

---

Home Index