---

Step * 2 of Lemma assert-es-first


1. es : EO
2. e : E
3. ∀[e':E]. ¬(e' < e) supposing loc(e') = loc(e) ∈ Id
⊢ ↑first(e)
BY
{ (SupposeNot THEN Auto THEN (FLemma `es-pred_property` [-1]⋅ THENA Auto) THEN InstHyp [⌈pred(e)⌉] 3⋅ THEN Auto) }

---

Latex:



1.  es  :  EO
2.  e  :  E
3.  \mforall{}[e':E].  \mneg{}(e'  <  e)  supposing  loc(e')  =  loc(e)
\mvdash{}  \muparrow{}first(e)


By

(SupposeNot
  THEN  Auto
  THEN  (FLemma  `es-pred\_property`  [-1]\mcdot{}  THENA  Auto)
  THEN  InstHyp  [\mkleeneopen{}pred(e)\mkleeneclose{}]  3\mcdot{}
  THEN  Auto)

---

Home Index