---

Step * of Lemma eo-forward-alle-lt

∀Info:Type. ∀es:EO+(Info). ∀b:E. ∀e:{e:E| b ≤loc e } .
  ∀[P:{e':E| b ≤loc e'  ∧ (e' <loc e)}  ─→ ℙ]. (∀e'<e.P[e'] ⇐⇒ ∀e':E. (b ≤loc e'  ⇒ (e' <loc e) ⇒ P[e']))
BY
{ (Unfold `alle-lt` 0 THEN Auto THEN RWW "eo-forward-locl" (-1) THEN Auto) }

---

Latex:


\mforall{}Info:Type.  \mforall{}es:EO+(Info).  \mforall{}b:E.  \mforall{}e:\{e:E|  b  \mleq{}loc  e  \}  .
    \mforall{}[P:\{e':E|  b  \mleq{}loc  e'    \mwedge{}  (e'  <loc  e)\}    {}\mrightarrow{}  \mBbbP{}]
        (\mforall{}e'<e.P[e']  \mLeftarrow{}{}\mRightarrow{}  \mforall{}e':E.  (b  \mleq{}loc  e'    {}\mRightarrow{}  (e'  <loc  e)  {}\mRightarrow{}  P[e']))


By

(Unfold  `alle-lt`  0  THEN  Auto  THEN  RWW  "eo-forward-locl"  (-1)  THEN  Auto)

---

Home Index