---

Step * of Lemma es-interval_wf

∀[es:EO]. ∀[e,e':E].  ([e, e'] ∈ E List)
BY
{ (Unfold `es-interval` 0 THEN Auto) }

---

Latex:


\mforall{}[es:EO].  \mforall{}[e,e':E].    ([e,  e']  \mmember{}  E  List)


By

(Unfold  `es-interval`  0  THEN  Auto)

---

Home Index