1. es : ES
2. e : E
3. e' : E
  (ev[e, e'].loc(ev) = loc(e')  Id)

By:	Unfold `l_all` 0 THEN RWO Thm* es:ES, e,e',ev:E. (ev  [e, e'])  e  ev  & ev  e'  -1 THEN Unfold `es-le` -1 THEN Unfold `es-locl` -1

1

4. ev : E 5. e  ev  6. loc(ev) = loc(e')  Id & (ev < e')  ev = e'   loc(ev) = loc(e')  Id

1 step

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