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

IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: set functionality wrt one one corr n pred

A:Type, B,B':(A

Prop).

(

x:A.

B(x)

B'(x))

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

By:	Auto THEN Rewrite by Thm* {x:A\| B(x) } ~ {x:A\| B(x) } THEN BackThru: 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 http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html