---

Step * of Lemma es-le-before-partition2

∀[es:EO]. ∀[e,a:E].  (≤loc(e) = (≤loc(pred(a)) @ [a, e]) ∈ (E List)) supposing ((¬↑first(a)) and a ≤loc e )
BY
{ (InstLemma `es-le-before-partition` []
   THEN RepeatFor 4 (ParallelLast')
   THEN Auto
   THEN HypSubst' -2 0
   THEN Auto
   THEN EqCD
   THEN Auto) }

---

Latex:


\mforall{}[es:EO].  \mforall{}[e,a:E].    (\mleq{}loc(e)  =  (\mleq{}loc(pred(a))  @  [a,  e]))  supposing  ((\mneg{}\muparrow{}first(a))  and  a  \mleq{}loc  e  )


By

(InstLemma  `es-le-before-partition`  []
  THEN  RepeatFor  4  (ParallelLast')
  THEN  Auto
  THEN  HypSubst'  -2  0
  THEN  Auto
  THEN  EqCD
  THEN  Auto)

---

Home Index