Def A == A  False

is mentioned by

Thm* a,p:. prime(p)  (CoPrime(p,a)  p | a)	[coprime_iff_ndivides]
Thm* p:. prime(p)  p = 0 & (p ~ 1) & (a:. a | p  (a ~ 1)  (a ~ p))	[prime_elim]
Thm* a:. atomic(a)  (a ~ 1) & (b:. b | a  (b ~ 1)  (b ~ a))	[atomic_char]
Thm* a:, b:. a | b & b | a  a<b & a | b	[pdivisor_bound]
Def prime(a) == a = 0 & (a ~ 1) & (b,c:. a | bc  a | b  a | c)	[prime]
Def atomic(a) == a = 0 & (a ~ 1) & reducible(a)	[atomic]
Def reducible(a) == b,c:. (b ~ 1) & (c ~ 1) & a = bc	[reducible]

In prior sections: core bool 1 int 2 rel 1

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