---

Step * 2 1 1 of Lemma null-es-hist


1. Info : Type
2. es : EO+(Info)@i'
3. e1 : E@i
4. e2 : E@i
5. loc(e2) = loc(e1) ∈ Id
6. ¬(e2 <loc e1)
7. [e1, e2] = [] ∈ (E List)
⊢ (e2 <loc e1)
BY
{ ((RWO "es-interval-nil" (-1)) THEN Auto) }

---

Latex:



1.  Info  :  Type
2.  es  :  EO+(Info)@i'
3.  e1  :  E@i
4.  e2  :  E@i
5.  loc(e2)  =  loc(e1)
6.  \mneg{}(e2  <loc  e1)
7.  [e1,  e2]  =  []
\mvdash{}  (e2  <loc  e1)


By

((RWO  "es-interval-nil"  (-1))  THEN  Auto)

---

Home Index