---

Step * of Lemma es-closed-open-interval-eq-before

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[e1,e2:E].  [e1;e2) = before(e2) ∈ (E List) supposing e1 ≤loc e2 
BY
{ (Auto THEN (RWO "eo-forward-before" 0 THENA Auto) THEN Try (Fold `es-closed-open-interval` 0) THEN Auto) }

---

Latex:


\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[e1,e2:E].    [e1;e2)  =  before(e2)  supposing  e1  \mleq{}loc  e2 


By

(Auto
  THEN  (RWO  "eo-forward-before"  0  THENA  Auto)
  THEN  Try  (Fold  `es-closed-open-interval`  0)
  THEN  Auto)

---

Home Index