Nuprl - Proof: hexists def 1

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

'a:S. (

p:'a

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

(

P:'a

. P(@

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

By:	HN THEN Simp THEN StrongAuto

Generated subgoal:

1 1. 'a : S
(p:'a. x:'a. (p(x))) = (P:'a. P(@x:'a. (P(x))))
5 steps

About:

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