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

None

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