(46steps total) PrintForm Definitions hol num Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: num iso 4 1 1
1. x : 
2. x':. x = rep_num(x')
  is_num_rep(rep_num(0))
By: Thin 2 THEN Unab [`hrep_num`] THEN Simp THEN StrongAuto
THEN
Unab [`his_num_rep`]
THEN
Simp
THEN
StrongAuto

Generated subgoals:

None

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

(46steps total) PrintForm Definitions hol num Sections HOLlib Doc