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. rcv(l; tg) : T(a)?Top
  a  dom(a : B)

By:	Unfolds [`fpf-dom`;`fpf-single`] 0 THEN Reduce 0 THEN RWO Thm* d:EqDecider(A), i:A. (eqof(d)(i,i)) ~ true 0 THEN Reduce 0

None

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