---

Step * 1 of Lemma existse-le-iff


1. es : EO@i'
2. e' : E@i
3. [P] : {e:E| loc(e) = loc(e') ∈ Id}  ⟶ ℙ
4. ∃e≤e'.P[e]@i
⊢ P[e'] ∨ ∃e<e'.P[e]
BY
{ ((((D (-1)) THEN ExRepD THEN (D (-2))) THENL [OrRight; OrLeft])
   THEN Auto
   THEN Unfold `existse-before` 0
   THEN (InstConcl [⌜e⌝])⋅
   THEN Auto) }

---

Latex:

---

Latex:

1.  es  :  EO@i'
2.  e'  :  E@i
3.  [P]  :  \{e:E|  loc(e)  =  loc(e')\}    {}\mrightarrow{}  \mBbbP{}
4.  \mexists{}e\mleq{}e'.P[e]@i
\mvdash{}  P[e']  \mvee{}  \mexists{}e<e'.P[e]


By

---

Latex:
((((D  (-1))  THEN  ExRepD  THEN  (D  (-2)))  THENL  [OrRight;  OrLeft])
  THEN  Auto
  THEN  Unfold  `existse-before`  0
  THEN  (InstConcl  [\mkleeneopen{}e\mkleeneclose{}])\mcdot{}
  THEN  Auto)

---

Home Index