i:Id, T:Type, v:T, x:Id.
  @i: x:T
  @i: xinitially x = v 
  realizes es.(vartype(i;x) r T)
  realizes es.& (e:E. loc(e) = i  Id  first(e)  (x when e) = v  T)

By:	Auto THEN BackThru Thm* 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) THENA Try (Complete Auto)

1	1. i : Id 2. T : Type{i} 3. v : T 4. x : Id   (es.(vartype(i;x) r T)   (& (e:E. loc(e) = i  Id  first(e)  (x when e) = v  T))    {es:ES| es is an event system of @i: x:T initially x = v }Prop{i'}	4 steps
2	1. i : Id 2. T : Type 3. v : T 4. x : Id   @i: x:T   @i: xinitially x = v realizes2 es.(vartype(i;x) r T)   & (e:E. loc(e) = i  Id  first(e)  (x when e) = v  T)	30 steps

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html