Nuprl - fun_1 LEMMAs for bij_imp_exists

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

Theorem	Name
Thm* f:(AB). Bij(A; B; f) (g:(BA). InvFuns(A; B; f; g))	[bij_imp_exists_inv]
cites the following:
Thm* Q:(ABProp). (x:A. y:B. Q(x,y)) (f:(AB). x:A. Q(x,f(x)))	[ax_choice]

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