Def AtomDeq == <a,b. a=bAtom,atom_DASH_deq_DASH_aux{1:l}>

is mentioned by

Def IdDeq == product-deq(Atom;;AtomDeq;NatDeq)

[id-deq]

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