---

Step * of Lemma decidable__es-locl

∀the_es:EO. ∀e',e:E.  Dec((e <loc e'))
BY
{ ((Auto THEN RWO "assert-es-bless<" 0) THEN Auto) }

---

Latex:


\mforall{}the$_{es}$:EO.  \mforall{}e',e:E.    Dec((e  <loc  e'))


By

((Auto  THEN  RWO  "assert-es-bless<"  0)  THEN  Auto)

---

Home Index