(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 2 1
1. x' : 
2. x'' : 
3. rep_num(x') = rep_num(x'')
4. m : 
5. n : 
6. m<n
7. rep_num(m) = rep_num(n)
  m = n
By: ((On [7;6;5] MoveToConcl) THEN (NInd 4)) THEN StrongAuto
THEN
Try (Complete (Unfold `label` 0))
THEN
HN

Generated subgoals:

1 4. n : 
5. 0<n
6. rep_num(0) = rep_num(n)  
  0 = n  
12 steps
2 4. m : 
5. 0<m
6. n:. m-1<n  rep_num(m-1) = rep_num(n)    m-1 = n  
7. n : 
8. m<n
9. rep_num(m) = rep_num(n)  
  m = n  
9 steps

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

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