---

Step * 2 of Lemma es-interval-eq


1. es : EO
2. e : E
⊢ [] @ filter(λev.e ≤loc ev;[e]) ~ [e]
BY
{ (((((Reduce 0 THEN SplitOnConclITE) THENA Auto) THEN Try (Trivial)) THENA Auto) THEN (D (-1)) THEN Auto) }

---

Latex:

---

Latex:

1.  es  :  EO
2.  e  :  E
\mvdash{}  []  @  filter(\mlambda{}ev.e  \mleq{}loc  ev;[e])  \msim{}  [e]


By

---

Latex:
(((((Reduce  0  THEN  SplitOnConclITE)  THENA  Auto)  THEN  Try  (Trivial))  THENA  Auto)
  THEN  (D  (-1))
  THEN  Auto)

---

Home Index