---

Step * of Lemma es-le-before-if-first

∀[es:EO]. ∀[e:E].  ≤loc(e) ~ [e] supposing ↑first(e)
BY
{ (Auto THEN Unfold `es-le-before` 0 THEN RWO "es-before-is-nil-if-first" 0 THEN Auto THEN Reduce 0 THEN Auto) }

---

Latex:


\mforall{}[es:EO].  \mforall{}[e:E].    \mleq{}loc(e)  \msim{}  [e]  supposing  \muparrow{}first(e)


By

(Auto
  THEN  Unfold  `es-le-before`  0
  THEN  RWO  "es-before-is-nil-if-first"  0
  THEN  Auto
  THEN  Reduce  0
  THEN  Auto)

---

Home Index