---

Step * of Lemma iseg-es-le-before

∀es:EO. ∀e',e:E.  (e' ≤loc e  ⇒ ≤loc(e') ≤ ≤loc(e))
BY
{ (Auto THEN D (-1)⋅ THEN Auto THEN Try ((HypSubst' (-1) 0 THEN Auto)) THEN Unfold `es-le-before` 0) }

1
1. es : EO@i'
2. e' : E@i
3. e : E@i
4. (e' <loc e)@i
⊢ before(e') @ [e'] ≤ before(e) @ [e]

---

Latex:


\mforall{}es:EO.  \mforall{}e',e:E.    (e'  \mleq{}loc  e    {}\mRightarrow{}  \mleq{}loc(e')  \mleq{}  \mleq{}loc(e))


By

(Auto  THEN  D  (-1)\mcdot{}  THEN  Auto  THEN  Try  ((HypSubst'  (-1)  0  THEN  Auto))  THEN  Unfold  `es-le-before`  0)

---

Home Index