---

Step * of Lemma es-first-at_wf

∀[es:EO]. ∀[i:Id]. ∀[e':E]. ∀[P:{e:E| loc(e) = i ∈ Id}  ─→ ℙ].  (e' is first@ i s.t.  e.P[e] ∈ ℙ)
BY
{ ((Auto THEN Unfold `es-first-at` 0 THEN UnivCD) THENA Auto) }

1
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'] ∈ ℙ

---

Latex:


\mforall{}[es:EO].  \mforall{}[i:Id].  \mforall{}[e':E].  \mforall{}[P:\{e:E|  loc(e)  =  i\}    {}\mrightarrow{}  \mBbbP{}].    (e'  is  first@  i  s.t.    e.P[e]  \mmember{}  \mBbbP{})


By

((Auto  THEN  Unfold  `es-first-at`  0  THEN  UnivCD)  THENA  Auto)

---

Home Index