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

is mentioned by

Def KindDeq == union-deq(IdLnkId;Id;product-deq(IdLnk;Id;IdLnkDeq;IdDeq);IdDeq)	[Kind-deq]
Def IdLnkDeq == product-deq(Id;Id;IdDeq;product-deq(Id;;IdDeq;NatDeq))	[idlnk-deq]
Def a = b == eqof(IdDeq)(a,b)	[eq_id]

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