---

Step * 2 of Lemma eo-forward-first2


1. Info : Type
2. eo : EO+(Info)
3. e : E
4. e' : {e':E| e' ≤loc e } 
5. e = e' ∈ E
⊢ ↑first(e)
BY
{ (D -2 THEN Unhide⋅ THEN Auto THEN Auto) }

1
1. Info : Type
2. eo : EO+(Info)
3. e : E
4. e' : E
5. e' ≤loc e 
6. e = e' ∈ E
⊢ ↑first(e)

---

Latex:



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


By

(D  -2  THEN  Unhide\mcdot{}  THEN  Auto  THEN  Auto)

---

Home Index