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

By:	NewSpecializeEsLemmaOn Thm* 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) x : T initially x = v

None

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