Nuprl - Proof: num iso 2 1 2

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

1. x' :

2. x'' :

3. rep_num(x') = rep_num(x'')
4. m :

5. 0<m
6.

. 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

By:	InstHyp [n-1] 6 THEN StrongAuto THEN Try (Complete (Unfold `label` 0))

Generated subgoal:

1 rep_num(m-1) = rep_num(n-1)
8 steps

About:

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