---

Step * 1 of Lemma alle-between2-false


1. es : EO@i'
2. e1 : E@i
3. e2 : {e:E| loc(e) = loc(e1) ∈ Id} @i
4. ∀e∈[e1,e2].False@i
⊢ (e2 <loc e1)
BY
{ (SupposeNot
   THEN (Unfold `alle-between2` (-2))
   THEN (InstHyp [⌜e1⌝] (-2))⋅
   THEN Auto
   THEN RWO "es-le-not-locl" 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  es  :  EO@i'
2.  e1  :  E@i
3.  e2  :  \{e:E|  loc(e)  =  loc(e1)\}  @i
4.  \mforall{}e\mmember{}[e1,e2].False@i
\mvdash{}  (e2  <loc  e1)


By

---

Latex:
(SupposeNot
  THEN  (Unfold  `alle-between2`  (-2))
  THEN  (InstHyp  [\mkleeneopen{}e1\mkleeneclose{}]  (-2))\mcdot{}
  THEN  Auto
  THEN  RWO  "es-le-not-locl"  0
  THEN  Auto)

---

Home Index