Def IdLnkDeq == product-deq(Id;Id;IdDeq;product-deq(Id;;IdDeq;NatDeq))

is mentioned by

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

Try larger context: EventSystems IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html