i:Id, L:Knd List, x:Id, T:Type.
  @i: only members of L affect x :T  Dsys
  & (D:Dsys. 
  & (@i: only members of L affect x :T  D
  & (
  & (D 
  & (realizes es.(vartype(i;x) r T)
  & (realizes es.& (e:E. 
  & (realizes es.& (loc(e) = i  Id
  & (realizes es.& (
  & (realizes es.& (((x after e) = (x when e)  T  (kind(e)  L))
  & (realizes es.& (& ((kind(e)  L)  (x after e) = (x when e)  T)))

None

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