i,a:Id, T:Type, ds:x:Id fp-> Type, P:(State(ds)
TProp),
Thm*
init:x:Id fp-> ds(x)?Void.
Thm* (
x:Id. x 
dom(ds) 
x dom(init))
Thm*
Thm* @i (with ds: ds
Thm* @i init: init
Thm* @i action a:T
Thm* @i precondition a(v) is
Thm* @i P s v)
Thm* realizes es.(
v:T. P((
x.init(x)?
),v)) (e:E. loc(e) = i Id)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
(EqDecider(B) 
r EqDecider(A))