Nuprl - Proof: hres exists wd 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hres exists wd 1

1. 'a : S
2. P : 'a

3. B : 'a

(

res_exists('a;x.P(x);x.B(x))) = (

x:'a. ((P(x))

(B(x))))

By:	Unab [`res_exists`] THEN Simpsetp [`bequal`] THEN StrongAuto THEN Try HypBackchain THEN StrongAuto

Generated subgoals:

None

About:

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