---

Step * of Lemma assert-es-first-locl

∀[es:EO]. ∀[e:E].  uiff(↑first(e);∀[e':E]. ¬(e' <loc e) supposing loc(e') = loc(e) ∈ Id)
BY
{ ((UnivCD THENA Auto) THEN (RWO "assert-es-first" 0 THEN Auto) THEN InstHyp [⌈e'⌉] (-3)⋅ THEN Auto) }

---

Latex:


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


By

((UnivCD  THENA  Auto)  THEN  (RWO  "assert-es-first"  0  THEN  Auto)  THEN  InstHyp  [\mkleeneopen{}e'\mkleeneclose{}]  (-3)\mcdot{}  THEN  Auto)

---

Home Index