Def  S  T == x:S. x  T

is mentioned by

Thm*  (x:A. B(x)  B'(x))  {x:A| B(x) }  {x:A| B'(x) }	[set_inc_wrt_imp_sq]
Thm*  (x:A. B(x)  B'(x))  {x:A| B(x) }  {x:A| B'(x) }	[set_inc_wrt_imp]

In prior sections: quot 1 int 1

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