---

Step * of Lemma es-interval-eq-le-before

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

---

Latex:


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


By

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

---

Home Index