PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: function functionality wrt one one corr B

  A:Type, B,B':(AType). (x:AB(x) ~ B'(x))  ((x:AB(x)) ~ (x:AB'(x)))

By: Auto
THEN
BackChainWithHyps: 
Thm*  (x:AB(x)) ~ (x:A'B'(x))  ((x:AB(x)) ~ (x:A'B'(x))) |
Thm*  (x:AB(x) ~ B'(x))  (x:AB(x)) ~ (x:AB'(x))


Generated subgoals:

None

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

PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc