1. Id
2. Id
3. x : Id
4. A : Type
5. T : Type
6. c : A
7. P : ATProp
8. (s,v. P(s(x),v))  State(x : A)TProp
9. x@0:Id. x@0  dom(x : A)  x@0  dom(x : c)
  x : c  x@0:Id fp-> x : A(x@0)?Void

By:	Assert (x : A  x:Id fp-> Type)

None

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