Def {!x:T | P(x)} == {x:T| P(x) & (y:T. P(y)  y = x) }

is mentioned

In prior sections: core

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