DiscreteMath
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Rank
Theorem
Name
4
Thm*
((
) ~
)
[not_nat_occ_natfuns]
cites the following:
3
Thm*
(
f
:(
A
B
). Bij(
A
;
B
;
f
))
(
B
~
A
)
[bij_iff_1_1_corr_version2a]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
DiscreteMath
Sections
DiscrMathExt
Doc
((
) ~ )
f:(AB). Bij(A; B; f)) 
(B ~ A)(() ~ )f:(AB). Bij(A; B; f)) (B ~ A)