mb event system 1 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def locl(a) == inr(a)

is mentioned by

Thm* a:Id, l:IdLnk, tg:Id. locl(a) = rcv(l; tg)  False[not_locl_rcv]
Thm* a:Id, l:IdLnk, tg:Id. rcv(l; tg) = locl(a)  False[not_rcv_locl]
Thm* a,b:Id. locl(a) = locl(b)  a = b[locl_one_one]

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