1. A : Type
2. B : Type
3. T : Type
4. x : Id
5. a : Knd
6. tg : Id
7. l : IdLnk
8. f : AB(T List)
9. a = rcv(l; tg)  T = B
10. x : A  x:Id fp-> Type
11. a : B  x:Knd fp-> Type
12. s : State(x : A)
13. v : if a  dom(a : B) B else rcv(l; tg) : T(a)?Top fi
14. f(s(x),v) = f(s(x),v)
15. T List
16. T List
17. u : T
  u  if rcv(l; tg)  dom(a : B) a : B(rcv(l; tg))?Void else T fi

1

18. rcv(l; tg)  dom(a : B)   u  a : B(rcv(l; tg))?Void

1 step

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