---

Step * 1 of Lemma es-pred?_property


1. es : EO@i'
2. e : E@i
3. ↑first(e)
⊢ ∀e':E. ¬(e' < e) supposing loc(e') = loc(e) ∈ Id
BY
{ (RWO "assert-es-first" (-1) THEN Auto) }

---

Latex:



1.  es  :  EO@i'
2.  e  :  E@i
3.  \muparrow{}first(e)
\mvdash{}  \mforall{}e':E.  \mneg{}(e'  <  e)  supposing  loc(e')  =  loc(e)


By

(RWO  "assert-es-first"  (-1)  THEN  Auto)

---

Home Index