Def NatDeq == <a,b. a=b,nat_DASH_deq_DASH_aux{1:l}>

is mentioned by

Def IdLnkDeq == product-deq(Id;Id;IdDeq;product-deq(Id;;IdDeq;NatDeq))	[idlnk-deq]
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