---

Step * of Lemma es-interface-predecessors-equal-subtype

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

---

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-equal`  []
  THEN  RepeatFor  6  ((ParallelLast'  THENA  Auto))
  THEN  Auto)

---

Home Index