i:Id, L:Knd List, x:Id, T:Type.
Thm* @i: only L affects x : T
Thm* realizes es.(vartype(i;x)
r T)
Thm* realizes es.& (
e:E.
Thm* realizes es.& (loc(e) = i
Id
Thm* realizes es.& (
Thm* realizes es.& ((
(x after e) = (x when e) T (kind(e) L))
Thm* realizes es.& (& (
(kind(e) L) (x after e) = (x when e) T))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)d:EqDecider(A), i:A. (eqof(d)(i,i)) ~ true
eq:EqDecider(A), L:A List, x:A. deq-member(eq;x;L) 
(x L)