PrintForm Definitions Lemmas hol arithmetic 4 Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: wop
  P:(). (n:. P(n))  (n:. P(n) & (m:. m<n  P(m)))
By: RewriteOfThm
Thm* all
Thm* (P:hnum  hbool. implies
Thm* (P:hnum  hbool. (exists(n:hnum. P(n))
Thm* (P:hnum  hbool. ,exists
Thm* (P:hnum  hbool. ,(n:hnum. and
Thm* (P:hnum  hbool. ,(n:hnum. (P(n)
Thm* (P:hnum  hbool. ,(n:hnum. ,all(m:hnum. implies(lt(m,n),not(P(m))))))))
(SimpsetC [`hol_to_nuprl`;`bequal`])

Generated subgoals:

None

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

PrintForm Definitions Lemmas hol arithmetic 4 Sections HOLlib Doc