Def A == A  False

is mentioned by

Thm* n:. n+1 = 0	[not_suc]
Def zero_rep == @x:. (y:. x = suc_rep(y)  )	[hzero_rep]
Def suc_rep == x:. (@f:. (one_one(;;f) & onto(;;f)))(x)	[hsuc_rep]

In prior sections: core bool 1 hol hol bool

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