---

Step * of Lemma es-interval_wf2

∀[es:EO]. ∀[e,e':E].  ([e, e'] ∈ {ev:E| loc(ev) = loc(e') ∈ Id}  List)
BY
{ (Auto THEN BLemma `list-set-type2` THEN Auto) }

1
1. es : EO
2. e : E
3. e' : E
⊢ (∀ev∈[e, e'].loc(ev) = loc(e') ∈ Id)

---

Latex:


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


By

(Auto  THEN  BLemma  `list-set-type2`  THEN  Auto)

---

Home Index