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

is mentioned by

Thm* a,b:Atom. a = b  a=bAtom	[atom-deq-aux]
Def AtomDeq == <a,b. a=bAtom,atom_DASH_deq_DASH_aux{1:l}>	[atom-deq]

In prior sections: bool 1 sqequal 1

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