---

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


1. es : EO
2. i : Id
3. P : {e:E| loc(e) = i ∈ Id}  ─→ ℙ
4. e1 : E
5. e2 : E
6. loc(e1) = i ∈ Id
7. P[e1]
8. ∀e'<e1.¬P[e']
9. loc(e2) = i ∈ Id
10. P[e2]
11. ∀e'<e2.¬P[e']
12. (e1 <loc e2)
⊢ e1 = e2 ∈ E
BY
{ (With ⌈e1⌉ (D (-2))⋅ THEN ThinTrivial THEN Auto) }

---

Latex:



1.  es  :  EO
2.  i  :  Id
3.  P  :  \{e:E|  loc(e)  =  i\}    {}\mrightarrow{}  \mBbbP{}
4.  e1  :  E
5.  e2  :  E
6.  loc(e1)  =  i
7.  P[e1]
8.  \mforall{}e'<e1.\mneg{}P[e']
9.  loc(e2)  =  i
10.  P[e2]
11.  \mforall{}e'<e2.\mneg{}P[e']
12.  (e1  <loc  e2)
\mvdash{}  e1  =  e2


By

(With  \mkleeneopen{}e1\mkleeneclose{}  (D  (-2))\mcdot{}  THEN  ThinTrivial  THEN  Auto)

---

Home Index