Nuprl - LogicSupplement LEMMAs for set_inc_wrt_imp_sq

LogicSupplement Sections DiscrMathExt Doc

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

Theorem	Name
Thm* (x:A. B(x) B'(x)) {x:A\| B(x) } {x:A\| B'(x) }	[set_inc_wrt_imp_sq]
cites the following:
Thm* x:{x:A\| B(x) }. B(x)	[subset_to_squash]
Thm* x:A. B(x) x {x:A\| B(x) }	[squash_to_subset]

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

LogicSupplement Sections DiscrMathExt Doc