---

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


1. Info : Type
2. eo : EO+(Info)
3. e : E
4. e' : E
5. (loc(e') = loc(e) ∈ Id) ⇒ e ≤loc e' 
⊢ e' ∈ {e':E| (loc(e') = loc(e) ∈ Id) ⇒ e ≤loc e' } 
BY
{ Auto }

---

Latex:



1.  Info  :  Type
2.  eo  :  EO+(Info)
3.  e  :  E
4.  e'  :  E
5.  (loc(e')  =  loc(e))  {}\mRightarrow{}  e  \mleq{}loc  e' 
\mvdash{}  e'  \mmember{}  \{e':E|  (loc(e')  =  loc(e))  {}\mRightarrow{}  e  \mleq{}loc  e'  \} 


By

Auto

---

Home Index