Def  x:A st P(x)B(x) == x:{x:A| P(x) }B(x)

is mentioned

In prior sections: DiscreteMath

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