IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
sub eq eq 0 m,n:. nnsub(m;n) = mm = 0 n = 0
By:
RewriteOfThm
Thm* all
Thm* (m:hnum. all(n:hnum. equal(equal(sub(m,n),m),or(equal(m,0),equal(n,0)))))
(SimpsetC [`hol_to_nuprl`;`bequal`])
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
m,n:
. nnsub(m;n) = m 
m = 0 
n = 0 
m:hnum. all(
