---

Step * 1 of Lemma parallel-classrel


1. T : Type
2. Info : Type
3. X : EClass(T)
4. Y : EClass(T)
5. es : EO+(Info)
6. e : E
7. v : T
8. v ∈ X || Y(e)
⊢ ↓v ∈ X(e) ∨ v ∈ Y(e)
BY
{ (RepUR ``classrel parallel-class eclass-compose2`` (-1)
   THEN (RWO "bag-member-append" (-1) THENA Auto)
   THEN Fold `classrel` (-1)
   THEN Auto) }

---

Latex:



1.  T  :  Type
2.  Info  :  Type
3.  X  :  EClass(T)
4.  Y  :  EClass(T)
5.  es  :  EO+(Info)
6.  e  :  E
7.  v  :  T
8.  v  \mmember{}  X  ||  Y(e)
\mvdash{}  \mdownarrow{}v  \mmember{}  X(e)  \mvee{}  v  \mmember{}  Y(e)


By

(RepUR  ``classrel  parallel-class  eclass-compose2``  (-1)
  THEN  (RWO  "bag-member-append"  (-1)  THENA  Auto)
  THEN  Fold  `classrel`  (-1)
  THEN  Auto)

---

Home Index