---

Step * 1 of Lemma alle-between1-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
{ ((((RWO "es-le-not-locl" 0 THENA Auto) THEN D 0) THENA Auto)
   THEN (Unfold `alle-between1` (-2))
   THEN (InstHyp [⌈e1⌉] (-2))⋅
   THEN Auto) }

---

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  \mleq{}loc  e1 


By

((((RWO  "es-le-not-locl"  0  THENA  Auto)  THEN  D  0)  THENA  Auto)
  THEN  (Unfold  `alle-between1`  (-2))
  THEN  (InstHyp  [\mkleeneopen{}e1\mkleeneclose{}]  (-2))\mcdot{}
  THEN  Auto)

---

Home Index