LogicSupplement Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
TheoremName
Thm*  (x:AB(x B'(x))  ({x:AB(x) } =ext {x:AB'(x) })[subset_exteq]
cites the following:
Thm*  (x:AB(x B'(x))  {x:AB(x) }  {x:AB'(x) }[set_inc_wrt_imp]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
LogicSupplement Sections DiscrMathExt Doc