Step * of Lemma iseg-es-le-before

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

1
1. es EO@i'
2. e' E@i
3. 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