Nuprl - Proof: hexists def 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hexists def 1 1

1. 'a : S

(

p:'a

x:'a. (p(x))) = (

P:'a

. P(@

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

By:	Simpset [`ext`] THEN Simp THEN StrongAuto

Generated subgoal:

1 2. P : 'a
(x:'a. (P(x))) = P(@x:'a. (P(x)))
4 steps

About:

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