---

Step * of Lemma es-interface-predecessors-equal

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[X,Y:EClass(Top)].
  ∀[e:E]. (≤(X)(e) = ≤(Y)(e) ∈ (E(X) List)) supposing ∀e:E. (↑e ∈b X ⇐⇒ ↑e ∈b Y)
BY
{ (InstLemma `es-interface-predecessors-sqequal` [] THEN RepeatFor 5 (ParallelLast')) }

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]. (≤(X)(e) ~ ≤(Y)(e))
⊢ ∀[e:E]. (≤(X)(e) = ≤(Y)(e) ∈ (E(X) List))

---

Latex:

---

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


By

---

Latex:
(InstLemma  `es-interface-predecessors-sqequal`  []  THEN  RepeatFor  5  (ParallelLast'))

---

Home Index