Def @i: only L sends on (l with tg)(j)
Def == if eqof(IdDeq)(j,i) only L sends on (l with tg) else  fi

is mentioned by

Thm* i:Id, L:Knd List, l:IdLnk, tg:Id. Thm* @i: only L sends on (l with tg)  Thm* realizes es.e:E. loc(e) = i  Id  null(sends(l,tg,e))  (kind(e)  L)

[sframe-rule]

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