Def  !x:A. P(x) == x:A. x is the x:A. P(x)

is mentioned by

Thm*  A,B:Type, P:(ABProp). Thm*  (x:A. !y:B. P(x,y))  (!f:(AB). x:A. P(x,f(x)))	[unique_indep_fun_description]
Thm*  (x:A. !y:B. P(x,y))  (f:(AB). x:A. P(x,f(x)))	[indep_fun_description]
Thm*  B:(AType), P:(x:AB(x)Prop). Thm*  (x:A. !y:B(x). P(x,y))  (!{f:(x:AB(x))| x:A. P(x,f(x)) })	[unique_fun_description2]
Thm*  B:(AType), P:(x:AB(x)Prop). Thm*  (x:A. !y:B(x). P(x,y))  (!f:(x:AB(x)). x:A. P(x,f(x)))	[unique_fun_description]
Thm*  (x:A. !y:B(x). P(x,y))  (f:(x:AB(x)). x:A. P(x,f(x)))	[fun_description]
Thm*  (!A)  (!x:A. True)	[inhabited_uniquely_vs_exists_unique]
Thm*  P:(AProp). (!u:A. P(u))  (y,z:A. P(y)  P(z)  y = z)	[exists_unique_elim]

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