PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: inv pair inv2
  A,B:Type. ((AB)) ~ (A ~ B)
By: SimilarTo: Thm*  (AB) ~ (A ~ B)

Generated subgoals:

None

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

PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc