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
8. e : E
9. e:E. loc(e) = i  (x when e)  T
10. e:E. loc(e) = i  (x after e)  T
  e  e' 
  
  loc(e') = i  Id
  
  (x after e') = (x when e)  T
  
  (ev:E. e  ev  & ev  e'  & (x after ev) = (x when ev)  T)

1	11. e  e'  12. loc(e') = i  Id 13. (x after e') = (x when e)  T   ev:E. e  ev  & ev  e'  & (x after ev) = (x when ev)  T	59 steps
2	11. e  e'  12. loc(e') = i  Id   loc(e) = i  Id	3 steps

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