Nuprl - Proof: num iso 2 1 1 1 1 2

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: num iso 2 1 1 1 1 2

3. n :

4. 0<n

x = suc_rep(y)

By:	Unab [`hsuc_rep`] THEN ChooseDC THEN StrongAuto THEN Try (Complete (Unfold `label` 0)) THEN Try (Complete (Unfold `label` 0))

Generated subgoals:

1 5. f :
6. one_one(;;f)
7. onto(;;f)
x:. y:. x = f(y)
1 step

2 f:(). one_one(;;f) & onto(;;f)
6 steps

About:

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

1	5. f : 6. one_one(;;f) 7. onto(;;f) x:. y:. x = f(y)	1 step
2	f:(). one_one(;;f) & onto(;;f)	6 steps