Nuprl - Proof: hsum axiom

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hsum axiom

'c,'b,'a:S.

all

(

f:'a

'c. all

(

f:'a

'c. (

g:'b

'c. exists_unique

(

f:'a

'c. (

g:'b

'c. (

h:hsum('a; 'b)

'c. and

(

f:'a

'c. (

g:'b

'c. (

h:hsum('a; 'b)

'c. (equal(o(h,inl),f)

(

f:'a

'c. (

g:'b

'c. (

h:hsum('a; 'b)

'c. ,equal(o(h,inr),g)))))

By:	HOL "hsum_axiom"

Generated subgoals:

None

About:

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