Nuprl - Proof: hexists unique def

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

'a:S.

equal

(exists_unique

P:'a

hbool. and

P:'a

hbool. (exists(P)

P:'a

hbool. ,all

P:'a

hbool. ,(

x:'a. all(

y:'a. implies(and(P(x),P(y)),equal(x,y))))))

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

Generated subgoal:

1 1. 'a : S
(p:'a. b_exists_unique('a;x.p(x)))
= (P:'a. (x:'a. (P(x)))(x,y:'a. ((P(x))(P(y)))(x = y)))
2 steps

About:

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