Def x:A. B(x) == x:AB(x)

is mentioned by

Thm* P,Q:(SProp). Thm* S = T  (x:S. P(x)  Q(x))  (x:S. P(x))  (y:T. Q(y))	[exists_functionality_wrt_implies]
Thm* P,Q:(SProp). Thm* S = T  (x:S. P(x)  Q(x))  ((x:S. P(x))  (y:T. Q(y)))	[exists_functionality_wrt_iff]
Thm* Q:(TProp). (x:T. Q(x))  (x:T. Q(x))	[not_over_exists]
Thm* B:(TProp). (x:T. A & B(x))  A & (x:T. B(x))	[exists_over_and_r]

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