---

Step * of Lemma es-interface-predecessors-nonnull

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[X:EClass(Top)]. ∀[e:E(X)].  (null(≤(X)(e)) ~ ff)
BY
{ (InstLemma `es-interface-predecessors-nonempty` [] THEN RepeatFor 4 (ParallelLast')) }

1
1. [Info] : Type
2. [es] : EO+(Info)
3. [X] : EClass(Top)
4. [e] : E(X)
5. 0 < ||≤(X)(e)||
⊢ null(≤(X)(e)) ~ ff

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[X:EClass(Top)].  \mforall{}[e:E(X)].    (null(\mleq{}(X)(e))  \msim{}  ff)


By

---

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

---

Home Index