Def  A == A

is mentioned by

Thm*  (A)  (!(AB))	[unique_fn_over_empty]
Thm*  (A)  (x:A. True)	[inhabited_vs_exists]
Thm*  F:(PropProp). (P:Prop. F(P))  (A:Type. F(A))	[inhab_rep_eqv]
Thm*  A:Type. P = (A)  Prop	[inhab_rep_axiom]
Thm*  (x:A. B(x))  ((x:AB(x)))	[inhab_choice]
Def  !A == {x:A| y:A. x = y }	[inhabited_uniquely]

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