---

Step * of Lemma es-interval-partition

∀[es:EO]. ∀[e',e,a:E].  [e, e'] = ([e, pred(a)] @ [a, e']) ∈ (E List) supposing (e <loc a) ∧ a ≤loc e' 
BY
{ (UniformUnivCD Auto THEN Repeat (MoveToConcl (-1))) }

1
∀es:EO. ∀e',e,a:E.  (((e <loc a) ∧ a ≤loc e' ) ⇒ ([e, e'] = ([e, pred(a)] @ [a, e']) ∈ (E List)))

---

Latex:


\mforall{}[es:EO].  \mforall{}[e',e,a:E].    [e,  e']  =  ([e,  pred(a)]  @  [a,  e'])  supposing  (e  <loc  a)  \mwedge{}  a  \mleq{}loc  e' 


By

(UniformUnivCD  Auto  THEN  Repeat  (MoveToConcl  (-1)))

---

Home Index