---

Step * 1 of Lemma parallel-class-zero


1. T : Type
2. Info : Type
3. X : EClass(T)
4. es : EO+(Info)
5. e : E
⊢ (X || Empty es e) = (X es e) ∈ bag(T)
BY
{ (RepUR ``parallel-class eclass-compose2 es-empty-interface`` 0 THEN RWO "bag-append-empty" 0 THEN Auto) }

---

Latex:



1.  T  :  Type
2.  Info  :  Type
3.  X  :  EClass(T)
4.  es  :  EO+(Info)
5.  e  :  E
\mvdash{}  (X  ||  Empty  es  e)  =  (X  es  e)


By

(RepUR  ``parallel-class  eclass-compose2  es-empty-interface``  0
  THEN  RWO  "bag-append-empty"  0
  THEN  Auto)

---

Home Index