Def S  T == x:S. x  T

is mentioned by

Thm* ds,ds':ltg:Id fp-> Type. ds  ds'  State(ds')  State(ds)

[ma-state-subtype2]

In prior sections: int 1

Try larger context: EventSystems IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html