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)D:Dsys, P:({es:ES| es is an event system of D }
Prop{i'}).
Thm* D realizes2 es.P(es)
D realizes es.P(es)eq:EqDecider(A), L:A List, x:A. deq-member(eq;x;L) 
(x L)d:EqDecider(A), i:A. (eqof(d)(i,i)) ~ true