---

Step * of Lemma parallel-classrel-weak

∀[T,Info:Type]. ∀[X,Y:EClass(T)]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[v:T].  (v ∈ X || Y(e) ⇐⇒ v ∈ X(e) ↓∨ v ∈ Y(e))
BY
{ (InstLemma `parallel-classrel` [] THEN RepeatFor 7 (ParallelLast')) }

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. uiff(v ∈ X || Y(e);v ∈ X(e) ↓∨ v ∈ Y(e))
⊢ v ∈ X || Y(e) ⇐⇒ v ∈ X(e) ↓∨ v ∈ Y(e)

---

Latex:


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


By

(InstLemma  `parallel-classrel`  []  THEN  RepeatFor  7  (ParallelLast'))

---

Home Index