Def  A == A  False

is mentioned by

Thm*  a:. prime(a)  (p:, q:. pp = aqq)	[primes_sqr_roots]
Thm*  (p:, q:. pp = 2qq)	[two_sqr_roots]
Thm*  P:(Prop). (x:. P(x)  (x':. x'<x & P(x')))  (x:. P(x))	[nat_descent]

In prior sections: core bool 1 rel 1 LogicSupplement int 2 num thy 1 SimpleMulFacts

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