mb event system 1 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def IdLnk == IdId

is mentioned by

Thm* a:Id, l:IdLnk, tg:Id. locl(a) = rcv(ltg False[not_locl_rcv]
Thm* a:Id, l:IdLnk, tg:Id. rcv(ltg) = locl(a False[not_rcv_locl]
Thm* l:IdLnk. lnk-inv(lnk-inv(l)) = l  IdLnk[lnk-inv-inv]
Thm* SQType(IdLnk)[IdLnk_sq]
Def Knd == (IdLnkId)+Id[Knd]
Def haslink(lm) == mlnk(m) = l[haslink]
Def Msg(M) == l:IdLnkt:IdM(l,t)[Msg]

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

mb event system 1 Sections EventSystems Doc