1. A : Type
2. B : Type
3. T : Type
4. x : Id
5. a : Knd
6. tg : Id
7. l : IdLnk
8. 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. State(x : A)
13. v : if a  dom(a : B) B else rcv(l; tg) : T(a)?Top fi
  v  B

1

13. rcv(l; tg) : T(a)?Top   a  dom(a : B)

1 step

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