IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/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 http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
and
(all(
n:hnum. equal(add(0,n),n))
