---

Step * 1 of Lemma es-le-first

.....truecase..... 
1. es : EO
2. j : E
3. e : E
4. e ≤loc j 
5. ↑first(j)
⊢ j = e ∈ E
BY
{ ((D -2 THEN Auto THEN RWO "es-locl-iff" (-2)) THEN Auto) }

---

Latex:


.....truecase..... 
1.  es  :  EO
2.  j  :  E
3.  e  :  E
4.  e  \mleq{}loc  j 
5.  \muparrow{}first(j)
\mvdash{}  j  =  e


By

((D  -2  THEN  Auto  THEN  RWO  "es-locl-iff"  (-2))  THEN  Auto)

---

Home Index