---

Step * of Lemma member-eo-strict-forward-E

∀[Info:Type]. ∀[eo:EO+(Info)]. ∀[e,e':E].  e' ∈ E supposing (loc(e') = loc(e) ∈ Id) ⇒ (e <loc e')
BY
{ (Auto
   THEN SubsumeC ⌈{e':E| (loc(e') = loc(e) ∈ Id) ⇒ (e <loc e')} ⌉⋅
   THEN Try ((BLemma `eo-strict-forward-E-subtype2`⋅ THENA Auto))
   THEN Auto) }

---

Latex:


\mforall{}[Info:Type].  \mforall{}[eo:EO+(Info)].  \mforall{}[e,e':E].    e'  \mmember{}  E  supposing  (loc(e')  =  loc(e))  {}\mRightarrow{}  (e  <loc  e')


By

(Auto
  THEN  SubsumeC  \mkleeneopen{}\{e':E|  (loc(e')  =  loc(e))  {}\mRightarrow{}  (e  <loc  e')\}  \mkleeneclose{}\mcdot{}
  THEN  Try  ((BLemma  `eo-strict-forward-E-subtype2`\mcdot{}  THENA  Auto))
  THEN  Auto)

---

Home Index