IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
hadd wd and
(all(n:hnum. equal(add(0,n),n))
,all(m:hnum. all(n:hnum. equal(add(suc(m),n),suc(add(m,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(add(0,n),n))
