---

Step * 2 of Lemma es-interval-eq2


1. es : EO
2. e : E
3. e' : E
4. e = 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:



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


By

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

---

Home Index