---

Step * of Lemma parallel-classrel

∀[T,Info:Type]. ∀[X,Y:EClass(T)]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[v:T].  uiff(v ∈ X || Y(e);v ∈ X(e) ↓∨ v ∈ Y(e))
BY
{ (Unfold `sq_or` 0 THEN Auto THEN Try ((Unhide THEN Auto))) }

1
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)

2
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(e) ∨ v ∈ Y(e)
⊢ v ∈ X || Y(e)

---

Latex:


\mforall{}[T,Info:Type].  \mforall{}[X,Y:EClass(T)].  \mforall{}[es:EO+(Info)].  \mforall{}[e:E].  \mforall{}[v:T].
    uiff(v  \mmember{}  X  ||  Y(e);v  \mmember{}  X(e)  \mdownarrow{}\mvee{}  v  \mmember{}  Y(e))


By

(Unfold  `sq\_or`  0  THEN  Auto  THEN  Try  ((Unhide  THEN  Auto)))

---

Home Index