(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. x : 
2. x':. x = rep_num(x')
  is_num_rep(x)
By: Assert (m:. is_num_rep(rep_num(m))) THEN Simp THEN StrongAuto

Generated subgoals:

1 3. m : 
  is_num_rep(rep_num(m))
7 steps
2 3. m:. is_num_rep(rep_num(m))
  is_num_rep(x)
2 steps

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

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