IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
num iso31 1. x : 2. P:(). P(zero_rep) & (n:. P(n) P(suc_rep(n))) P(x)
x':. x = rep_num(x')
By:
InstHyp [x:. (x':. x = rep_num(x'))] 2 THEN Simp THEN StrongAuto
THEN
Try (Complete (Unfold `hnum` 0))