Nuprl - LogicSupplement LEMMAs for indep_fun_description

LogicSupplement Sections DiscrMathExt Doc

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

Rank	Theorem	Name
2	Thm* (x:A. !y:B. P(x,y)) (f:(AB). x:A. P(x,f(x)))	[indep_fun_description]
cites the following:
1	Thm* (x:A. y:B. Q(x,y)) (f:(AB). x:A. Q(x,f(x)))	[ax_choice_version2]

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

LogicSupplement Sections DiscrMathExt Doc