Def A == A  False

is mentioned by

Thm* (P  Q)  P  Q	[not_functionality_wrt_implies]
Thm* (P  Q)  (P  Q)	[not_functionality_wrt_iff]
Thm* Q:(TProp). (x:T. Q(x))  (x:T. Q(x))	[not_over_exists]
Thm* Dec(A)  ((A & B)  A  B)	[not_over_and]
Thm* A  B  (A & B)	[not_over_and_b]
Thm* (A  B)  A & B	[not_over_or_a]
Thm* (A  B)  A & B	[not_over_or]
Thm* Dec(A)  (A  A)	[dneg_elim_a]
Thm* Dec(A)  A  A	[dneg_elim]
Thm* SqStable(P)	[sq_stable__not]
Thm* Stable{P}	[stable__not]
Def Stable{P} == P  P	[stable]
Def Dec(P) == P  P	[decidable]
Def AB == B<A	[le]
Def a  b  T == a = b  T	[nequal]

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