Def KindDeq == union-deq(IdLnkId;Id;product-deq(IdLnk;Id;IdLnkDeq;IdDeq);IdDeq)

is mentioned by

Thm* ltg:(IdLnkIdType), i:Id, da1,da2:k:Knd fp-> Type. Thm* (ltg  da-outlinks(da1  da2;i)) Thm*  Thm* (ltg  da-outlinks(da1;i))  (ltg  da-outlinks(da2;i))	[da-outlinks-join]
Thm* da:k:Knd fp-> Type, k:{k:Knd| k  dom(da) & isrcv(k) }. Thm* da-outlink-f(da;k)  IdLnkIdType	[da-outlink-f_wf]

In prior sections: mb event system 2 mb event system 4

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