IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
hmult exp mono all
(p:hnum. all
(p:hnum. (q:hnum. all
(p:hnum. (q:hnum. (n:hnum. all
(p:hnum. (q:hnum. (n:hnum. (m:hnum. equal
(p:hnum. (q:hnum. (n:hnum. (m:hnum. (equal
(p:hnum. (q:hnum. (n:hnum. (m:hnum. ((mult(n,exp(suc(q),p))
(p:hnum. (q:hnum. (n:hnum. (m:hnum. (,mult(m,exp(suc(q),p)))
(p:hnum. (q:hnum. (n:hnum. (m:hnum. ,equal(n,m))))))
By:
HOL "hmult_exp_mono"
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
all
(
p:hnum. all
