---

Step * of Lemma es-interval-eq2

∀[es:EO]. ∀[e,e':E].  [e, e'] ~ [e'] supposing e = e' ∈ E
BY
{ ((((UnivCD THENA Auto) THEN Unfold `es-interval` 0 THEN RWO "filter_append" 0) THENA Auto)
   THEN Subst filter(λev.e ≤loc ev;before(e')) ~ [] 0⋅
   ) }

1
.....equality..... 
1. es : EO
2. e : E
3. e' : E
4. e = e' ∈ E
⊢ filter(λev.e ≤loc ev;before(e')) ~ []

2
1. es : EO
2. e : E
3. e' : E
4. e = e' ∈ E
⊢ [] @ filter(λev.e ≤loc ev;[e']) ~ [e']

---

Latex:


\mforall{}[es:EO].  \mforall{}[e,e':E].    [e,  e']  \msim{}  [e']  supposing  e  =  e'


By

((((UnivCD  THENA  Auto)  THEN  Unfold  `es-interval`  0  THEN  RWO  "filter\_append"  0)  THENA  Auto)
  THEN  Subst  filter(\mlambda{}ev.e  \mleq{}loc  ev;before(e'))  \msim{}  []  0\mcdot{}
  )

---

Home Index