Nuprl - LogicSupplement LEMMAs for fun_description

LogicSupplement Sections DiscrMathExt Doc

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

Theorem	Name
Thm* (x:A. !y:B(x). P(x,y)) (f:(x:AB(x)). x:A. P(x,f(x)))	[fun_description]
cites the following:
Thm* (x:A. y:B(x). Q(x,y)) (f:(x:AB(x)). x:A. Q(x,f(x)))	[dep_ax_choice_version2]

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

LogicSupplement Sections DiscrMathExt Doc