---

Step * of Lemma es-interval-is-nil

∀[es:EO]. ∀[e,e':E].  ([e, e'] ~ []) supposing ((e' <loc e) and (loc(e) = loc(e') ∈ Id))
BY
{ (UnivCD THENA Auto) }

1
1. es : EO
2. e : E
3. e' : E
4. loc(e) = loc(e') ∈ Id
5. (e' <loc e)
⊢ [e, e'] ~ []

---

Latex:


\mforall{}[es:EO].  \mforall{}[e,e':E].    ([e,  e']  \msim{}  [])  supposing  ((e'  <loc  e)  and  (loc(e)  =  loc(e')))


By

(UnivCD  THENA  Auto)

---

Home Index