1. es : ES
2. e : E
3. e' : E
4. ev : E
  (ev  [e, e'])  e  ev  & ev  e' 

By:

((Unfold `es-interval` 0 ((THEN ((RWO Thm* P:(T), L:T List, x:T. (x  filter(P;L))  (x  L) & P(x) 0) (THEN ((Reduce 0) (THEN ((RWO Thm* x:T, l1,l2:T List. (x  l1 @ l2)  (x  l1)  (x  l2) 0) (THEN ((RWO Thm* the_es:ES, e',e:E. (e  before(e'))  (e <loc e') 0) (THEN ((RWO Thm* l:T List, a,x:T. (x  [a / l])  x = a  (x  l) 0) (THEN ((RWO Thm* x:T. (x  nil)  False 0) (THEN ((RWO Thm* es:ES, e,e':E. es-ble{i:l}(es;e;e')  e  e'  0)) THENA Reduce 0

1

(ev <loc e')  ev = e'  False & e  ev   e  ev  & ev  e'

3 steps

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html