DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
RankTheoremName
2Thm*  ((AB)) ~ (A ~ B)[inv_pair_inv2]
cites the following:
1Thm*  (AB) ~ (A ~ B)[inv_pair_inv]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
DiscreteMath Sections DiscrMathExt Doc