---

Step * of Lemma es-le-before_wf

∀[es:EO]. ∀[e:E].  (≤loc(e) ∈ {a:E| loc(a) = loc(e) ∈ Id}  List)
BY
{ (Unfold `es-le-before` 0 THEN Auto) }

---

Latex:


\mforall{}[es:EO].  \mforall{}[e:E].    (\mleq{}loc(e)  \mmember{}  \{a:E|  loc(a)  =  loc(e)\}    List)


By

(Unfold  `es-le-before`  0  THEN  Auto)

---

Home Index