---

Step * of Lemma es-le-before_wf2

∀[es:EO]. ∀[e:E].  (≤loc(e) ∈ {a:E| a ≤loc e }  List)
BY
{ (Auto
   THEN BLemma `list_set_type`
   THEN Auto
   THEN BLemma `l_all_iff`
   THEN Auto
   THEN BLemma `member-es-le-before`⋅
   THEN Auto) }

---

Latex:


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


By

(Auto
  THEN  BLemma  `list\_set\_type`
  THEN  Auto
  THEN  BLemma  `l\_all\_iff`
  THEN  Auto
  THEN  BLemma  `member-es-le-before`\mcdot{}
  THEN  Auto)

---

Home Index