i:Id, T:Type, v:T, x:Id.
Thm* @i: x:T
Thm* @i: xinitially x = v
Thm* realizes es.(vartype(i;x)
r T)
Thm* realizes es.& (
e:E. loc(e) = i 
Id 
first(e) (x when e) = v 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