IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
hmult wd and
(all(n:hnum. equal(mult(0,n),0))
,all(m:hnum. all(n:hnum. equal(mult(suc(m),n),add(mult(m,n),n)))))
By:
HN
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
and
(all(
n:hnum. equal(mult(0,n),0))
