---

Step * of Lemma es-first-at-unique

∀[es:EO]. ∀[i:Id]. ∀[P:{e:E| loc(e) = i ∈ Id}  ─→ ℙ]. ∀[e1,e2:E].
  (e1 = e2 ∈ E) supposing (e2 is first@ i s.t.  e.P[e] and e1 is first@ i s.t.  e.P[e])
BY
{ (Auto THEN D -2 THEN D -1 THEN (InstLemma `es-locl-total` [⌈es⌉;⌈e1⌉;⌈e2⌉]⋅ THENM SplitOrHyps) THEN Auto) }

1
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

2
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. (e2 <loc e1)
⊢ e1 = e2 ∈ E

---

Latex:


\mforall{}[es:EO].  \mforall{}[i:Id].  \mforall{}[P:\{e:E|  loc(e)  =  i\}    {}\mrightarrow{}  \mBbbP{}].  \mforall{}[e1,e2:E].
    (e1  =  e2)  supposing  (e2  is  first@  i  s.t.    e.P[e]  and  e1  is  first@  i  s.t.    e.P[e])


By

(Auto
  THEN  D  -2
  THEN  D  -1
  THEN  (InstLemma  `es-locl-total`  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e1\mkleeneclose{};\mkleeneopen{}e2\mkleeneclose{}]\mcdot{}  THENM  SplitOrHyps)
  THEN  Auto)

---

Home Index