Nuprl - Proof: hadd sub

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

all(

a:hnum. all(

c:hnum. equal(sub(add(a,c),c),a)))

By:	HOL "hadd_sub"

Generated subgoals:

None

About:

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