---

Step * 1 1 1 of Lemma es-interval-eq


1. es : EO
2. e : E
⊢ (∀x∈before(e).¬↑((λev.e ≤loc ev) x))
BY
{ (Reduce 0 THEN BLemma `l_all_iff` THEN Auto) }

1
1. es : EO
2. e : E
3. x : E@i
4. (x ∈ before(e))@i
⊢ ¬↑e ≤loc x

---

Latex:



1.  es  :  EO
2.  e  :  E
\mvdash{}  (\mforall{}x\mmember{}before(e).\mneg{}\muparrow{}((\mlambda{}ev.e  \mleq{}loc  ev)  x))


By

(Reduce  0  THEN  BLemma  `l\_all\_iff`  THEN  Auto)

---

Home Index