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
11. e  e' 
12. loc(e') = i
13. (x after e') = (x when e)
14. ev : {e:E| loc(e) = i }
15. (ev  [e, e'])
16. (x after ev) = (x when ev)
17. e1 : E
18. e  e1  & e1  e' 
  (x after e1)  T

1	18. e  e1  19. loc(e1) = loc(e')  Id 20. (e1 < e')   vartype(loc(e1);x) r T	1 step
2	18. e  e1  19. e1 = e'   vartype(loc(e1);x) r T	1 step

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