Nuprl - Proof: hexists unique def 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hexists unique def 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)))

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

Generated subgoal:

1   (p:'a. b_exists_unique('a;x.p(x)))
  =
  (P:'a. (x:'a. (P(x)))(x,y:'a.  ((P(x))(P(y)))(x = y)))
1 step

About:

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