Nuprl - Proof: one one corr 2 functionality wrt eq

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: one one corr 2 functionality wrt eq

A,A',B,B':Type. A = A'

B = B'

(A ~ B) = (A' ~ B')

By:

UnivCD

Generated subgoal:

1 1. A : Type
2. A' : Type
3. B : Type
4. B' : Type
5. A = A'
6. B = B'
(A ~ B) = (A' ~ B')
1 step

About:

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