DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
RankTheoremName
2Thm*  Bij(; nat_to_nat_pair)[nat_to_nat_pair_bij]
cites the following:
1Thm*  Inj(; nat_to_nat_pair)[nat_to_nat_pair_inj]
0Thm*  Surj(; nat_to_nat_pair)[nat_to_nat_pair_surj]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
DiscreteMath Sections DiscrMathExt Doc