Nuprl - LogicSupplement LEMMAs for ax_choice_version3

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. Q(x,y)) (f:(AB). x:A. Q(x,f(x)))	[ax_choice_version3]
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