Subtypes by Comprehension - sometimes called "set types"

(x  A)

It is the type of a  A such that B(a).

Note that "a  {x:A| B(x) }" is not equivalent to "B(a)", since "B(a)" can be assigned a meaning for any a  A, but "a  {x:A| B(x) }" is not assigned a meaning unless it is true, i.e., when "B(a)" is true.

See Polymorphism, Equality, Types and Guarded Types.

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