Nuprl - Proof: his pair def

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

'a,'b:S.

all

(

p:'a

hbool. equal

(

p:'a

hbool. (is_pair(p)

(

p:'a

hbool. ,exists(

x:'a. exists(

y:'b. equal(p,mk_pair(x,y))))))

By:	HN THEN StrongAuto THEN Unab [`his_pair`] THEN Simp THEN StrongAuto

Generated subgoals:

None

About:

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