---

Step * of Lemma assert-es-first

∀[es:EO]. ∀[e:E].  uiff(↑first(e);∀[e':E]. ¬(e' < e) supposing loc(e') = loc(e) ∈ Id)
BY
{ Auto }

1
1. es : EO
2. e : E
3. ↑first(e)
4. e' : E
5. loc(e') = loc(e) ∈ Id
⊢ ¬(e' < e)

2
1. es : EO
2. e : E
3. ∀[e':E]. ¬(e' < e) supposing loc(e') = loc(e) ∈ Id
⊢ ↑first(e)

---

Latex:


\mforall{}[es:EO].  \mforall{}[e:E].    uiff(\muparrow{}first(e);\mforall{}[e':E].  \mneg{}(e'  <  e)  supposing  loc(e')  =  loc(e))


By

Auto

---

Home Index