Def  !A == {x:A| y:A. x = y }

is mentioned by

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*  (!A)  (!x:A. True)	[inhabited_uniquely_vs_exists_unique]
Thm*  P:(AType). (x:A. Dec(P(x)))  (!{p:(A)| x:A. p(x)  P(x) })	[dec_pred_imp_bool_decider_exists]
Thm*  (A)  (!(AB))	[unique_fn_over_empty]
Thm*  (!A)  (x:A. y:A. x = y)	[inhabited_uniquely_elim]
Thm*  (!A)  (x:A. y:A. x = y)	[inhabited_uniquely_vs_exists]

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