DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
RankTheoremName
4Thm*  Unbounded(A Finite(A)[unb_inf_not_fin]
cites the following:
3Thm*  ((m inj k))  mk[inj_typing_imp_le]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
DiscreteMath Sections DiscrMathExt Doc