Def a = !x:T. Q(x) == Q(a) & (a':T. Q(a')  a' = a)

is mentioned by

Thm* a:T, Q:(TProp). (a = !x:T. Q(x))  a  {!x:T | Q(x)}

[uni_sat_imp_in_uni_set]

Try larger context: StandardLIB IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html