1. i : Id
2. T : Type
3. v : T
4. x : Id
5. es : ES
6. w : World
7. p : FairFifo
8. PossibleWorld(@i: x:T
8. PossibleWorld(@i: xinitially x = v;w)
9. es = ES(w)
10. vartype(i;x) r T
11. e : E
12. loc(e) = i
13. first(e)
  (x when e)  T

1	(x when e)  vartype(loc(e);x)	1 step
2	vartype(loc(e);x) r T	1 step

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