---

Step * 1 of Lemma es-first-at_wf


1. es : EO
2. i : Id
3. e' : E
4. P : {e:E| loc(e) = i ∈ Id}  ─→ ℙ
⊢ (loc(e') = i ∈ Id) ∧ P[e'] ∧ ∀e'<e'.¬P[e'] ∈ ℙ
BY
{ (Unfolds ``and alle-lt`` 0 THEN Fold `cand` 0 THEN Auto THEN MemTypeCD THEN Auto) }

---

Latex:



1.  es  :  EO
2.  i  :  Id
3.  e'  :  E
4.  P  :  \{e:E|  loc(e)  =  i\}    {}\mrightarrow{}  \mBbbP{}
\mvdash{}  (loc(e')  =  i)  \mwedge{}  P[e']  \mwedge{}  \mforall{}e'<e'.\mneg{}P[e']  \mmember{}  \mBbbP{}


By

(Unfolds  ``and  alle-lt``  0  THEN  Fold  `cand`  0  THEN  Auto  THEN  MemTypeCD  THEN  Auto)

---

Home Index