---

Step * 1 of Lemma es-closed-open-interval-forward


1. Info : Type
2. es : EO+(Info)
3. e1 : E
4. e2 : E
5. e : E
6. e1 ≤loc e2 
7. e ≤loc e1 
8. es.e.e1 = es.e1 ∈ EO+(Info)
⊢ before(e2) = before(e2) ∈ (E List)
BY
{ Auto }

---

Latex:



1.  Info  :  Type
2.  es  :  EO+(Info)
3.  e1  :  E
4.  e2  :  E
5.  e  :  E
6.  e1  \mleq{}loc  e2 
7.  e  \mleq{}loc  e1 
8.  es.e.e1  =  es.e1
\mvdash{}  before(e2)  =  before(e2)


By

Auto

---

Home Index