IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
hsub plus all
(a:hnum. all(b:hnum. all(c:hnum. equal(sub(a,add(b,c)),sub(sub(a,b),c)))))
By:
HOL "hsub_plus"
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
all
(
a:hnum. all(
