Def x=yAtom == if x=yAtomtrue; false fi

is mentioned by

Thm* x,y:Atom. x=yAtom  x  y	[neg_assert_of_eq_atom]
Thm* x,y:Atom. x=yAtom  x = y	[assert_of_eq_atom]

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