Nuprl - Proof: function functionality wrt one one corr B

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':(A

Type). (

x:A. B(x) ~ B'(x))

((x:A

B(x)) ~ (x:A

B'(x)))

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

Generated subgoals:

None

About:

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