---

Step * of Lemma es-le-before-not-null

∀[es:EO]. ∀[e:E].  (null(≤loc(e)) ~ ff)
BY
{ (Unfold `es-le-before` 0 THEN Auto) }

---

Latex:


\mforall{}[es:EO].  \mforall{}[e:E].    (null(\mleq{}loc(e))  \msim{}  ff)


By

(Unfold  `es-le-before`  0  THEN  Auto)

---

Home Index