---

Step * of Lemma assert-es-ble

∀es:EO. ∀e,e':E.  (↑e ≤loc e' ⇐⇒ e ≤loc e' )
BY
{ ((UnivCD THENA Auto)
   THEN (RepUR ``es-ble es-le`` 0 THEN (RW assert_pushdownC 0 THENA Auto))
   THEN RWO "assert-es-bless" 0
   THEN Auto) }

---

Latex:


\mforall{}es:EO.  \mforall{}e,e':E.    (\muparrow{}e  \mleq{}loc  e'  \mLeftarrow{}{}\mRightarrow{}  e  \mleq{}loc  e'  )


By

((UnivCD  THENA  Auto)
  THEN  (RepUR  ``es-ble  es-le``  0  THEN  (RW  assert\_pushdownC  0  THENA  Auto))
  THEN  RWO  "assert-es-bless"  0
  THEN  Auto)

---

Home Index