Nuprl - Proof: one one corr fams if one one corr B

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: one one corr fams if 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

Generated subgoal:

1 1. A : Type
2. B : AType
3. B' : AType
4. x:A. B(x) ~ B'(x)
(x:A. B(x)) ~ (x:A. B'(x))
5 steps

About:

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