---

Step * of Lemma es-interface-predecessors-sqequal

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[X,Y:EClass(Top)].  ∀[e:E]. (≤(X)(e) ~ ≤(Y)(e)) supposing ∀e:E. (↑e ∈b X ⇐⇒ ↑e ∈b Y)
BY
{ ((UnivCD THENA Auto) THEN RepUR ``eclass-events es-interface-predecessors es-le-before`` 0) }

1
1. Info : Type
2. es : EO+(Info)
3. X : EClass(Top)
4. Y : EClass(Top)
5. ∀e:E. (↑e ∈b X ⇐⇒ ↑e ∈b Y)
6. e : E
⊢ filter(λe.e ∈b X;before(e) @ [e]) ~ filter(λe.e ∈b Y;before(e) @ [e])

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[X,Y:EClass(Top)].
    \mforall{}[e:E].  (\mleq{}(X)(e)  \msim{}  \mleq{}(Y)(e))  supposing  \mforall{}e:E.  (\muparrow{}e  \mmember{}\msubb{}  X  \mLeftarrow{}{}\mRightarrow{}  \muparrow{}e  \mmember{}\msubb{}  Y)


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  RepUR  ``eclass-events  es-interface-predecessors  es-le-before``  0)

---

Home Index