---

Step * of Lemma parallel-class-assoc

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

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  RepUR  ``parallel-class  eclass-compose2  eclass``  0
  THEN  RepeatFor  2  ((EqCD  THENA  Auto))
  THEN  RWO  "bag-append-assoc"  0
  THEN  Auto)

---

Home Index