1. es : ES
2. x : Id
3. i : Id
4. T : Type
5. x,y:T. Dec(x = y)
6. vartype(i;x) r T
7. e:E. loc(e) = i  (x when e)  T
8. e:E. loc(e) = i  (x after e)  T
9. WellFnd{i}(E;x,y.(x <loc y))
10. j : E
11. k:E. 
11. (k <loc j)
11. 
11. (e:E. 
11. (e  k 
11. (
11. (loc(k) = i
11. (
11. ((ev[e, k].(x after ev) = (x when ev))  (x after k) = (x when e))
12. e : E
13. (e <loc j)
14. loc(j) = i
15. (ev[e, j].(x after ev) = (x when ev))
16. (x after j) = (x when j)
17. loc(e) = i
18. first(j)
19. (x when j) = (x after pred(j))
  [e, pred(j)]  {e:E| loc(e) = i  Id } List

By:	Inst Thm* es:ES, e,e':E. [e, e']  {ev:E| loc(ev) = loc(e')  Id } List [es;e;pred(j)] THEN RWO Thm* the_es:ES, e:E. first(e)  loc(pred(e)) = loc(e)  Id -1 THEN DoSubsume

1

20. [e, pred(j)]  {ev:E| loc(ev) = loc(j)  Id } List   ({ev:E| loc(ev) = loc(j)  Id } List) r ({e:E| loc(e) = i  Id } List)

1 step

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