Def res_exists == P:'a. Q:'a. res_exists('a;x.(P(x));x.(Q(x)))

is mentioned

In prior sections: hol restr binder

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