Nuprl - Proof: hexp add

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

all

(

p:hnum. all

(

p:hnum. (

q:hnum. all

(

p:hnum. (

q:hnum. (

n:hnum. equal

(

p:hnum. (

q:hnum. (

n:hnum. (exp(n,add(p,q))

(

p:hnum. (

q:hnum. (

n:hnum. ,mult(exp(n,p),exp(n,q))))))

By:	HOL "hexp_add"

Generated subgoals:

None

About:

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