PrintForm Definitions Lemmas hol arithmetic 4 Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: pre sub
  m,n:. pre(nnsub(m;n)) = nnsub(pre(m);n)
By: RewriteOfThm Thm* all(m:hnum. all(n:hnum. equal(pre(sub(m,n)),sub(pre(m),n))))
(SimpsetC [`hol_to_nuprl`;`bequal`])

Generated subgoals:

None

About:
assertapplyequalall
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

PrintForm Definitions Lemmas hol arithmetic 4 Sections HOLlib Doc