Nuprl - Proof: set functionality wrt one one corr n pred2

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

A:Type, B,B':(A

Prop).

(

x:A. B(x)

B'(x))

({x:A| B(x) } ~ {x:A| B'(x) })

By:

Auto

Generated subgoal:

1 1. A : Type
2. B : AProp
3. B' : AProp
4. x:A. B(x) B'(x)
{x:A| B(x) } ~ {x:A| B'(x) }
3 steps

About:

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