Def S  T == x:S. x  T

is mentioned by

Def S  T == T  S

[suptype]

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