---

Step * 1 1 of Lemma es-first-at-exists2


1. es : EO@i'
2. i : Id@i
3. [P] : {e:E| loc(e) = i ∈ Id}  ─→ ℙ
4. ∀e:{e:E| loc(e) = i ∈ Id} . Dec(P[e])@i
5. e : E@i
6. loc(e) = i ∈ Id
7. ¬∀e'≤e.¬P[e']
8. e' : E
9. e' ≤loc e 
10. P[e']
⊢ ∃e'≤e.e' is first@ i s.t.  e'.P[e']
BY
{ (Assert loc(e') = i ∈ Id BY
         Auto) }

1
1. es : EO@i'
2. i : Id@i
3. [P] : {e:E| loc(e) = i ∈ Id}  ─→ ℙ
4. ∀e:{e:E| loc(e) = i ∈ Id} . Dec(P[e])@i
5. e : E@i
6. loc(e) = i ∈ Id
7. ¬∀e'≤e.¬P[e']
8. e' : E
9. e' ≤loc e 
10. P[e']
11. loc(e') = i ∈ Id
⊢ ∃e'≤e.e' is first@ i s.t.  e'.P[e']

---

Latex:



1.  es  :  EO@i'
2.  i  :  Id@i
3.  [P]  :  \{e:E|  loc(e)  =  i\}    {}\mrightarrow{}  \mBbbP{}
4.  \mforall{}e:\{e:E|  loc(e)  =  i\}  .  Dec(P[e])@i
5.  e  :  E@i
6.  loc(e)  =  i
7.  \mneg{}\mforall{}e'\mleq{}e.\mneg{}P[e']
8.  e'  :  E
9.  e'  \mleq{}loc  e 
10.  P[e']
\mvdash{}  \mexists{}e'\mleq{}e.e'  is  first@  i  s.t.    e'.P[e']


By

(Assert  loc(e')  =  i  BY
              Auto)

---

Home Index