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

None

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