---

Step * of Lemma es-blocl-is-bless

∀es:EO. ∀e,e':E.  (e <loc e' ~ es-blocl(es;e;e'))
BY
{ Auto }

---

Latex:


\mforall{}es:EO.  \mforall{}e,e':E.    (e  <loc  e'  \msim{}  es-blocl(es;e;e'))


By

Auto

---

Home Index