---

Step * of Lemma es-le-before-partition

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

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

---

Latex:

---

Latex:
\mforall{}[es:EO].  \mforall{}[e,a:E].    \mleq{}loc(e)  =  (before(a)  @  [a,  e])  supposing  a  \mleq{}loc  e 


By

---

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

---

Home Index