Def S  T == x:S. x  T

is mentioned by

Thm* A  Top	[sfa_doc_top_is_top]
Thm* Void  A	[sfa_doc_void_is_bottom]
Thm* k:.   ( mod k)	[sfa_doc_int_sub_int_mod]
Thm* B:(AType), a:A. (x:A. B(x))  B(a)	[sfa_doc_isect_subtype]

In prior sections: int 1

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