Nuprl - Proof: num iso 2 2 2

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

1. x' :

2. x'' :

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

m,n:

. m<n

rep_num(m) = rep_num(n)

m = n
5.

x'<x''

x' = x''

By:	Decide (x'>x'') THEN StrongAuto THEN Try (Complete (Unfold `label` 0))

Generated subgoal:

1 6. x'>x''
x' = x''
1 step

About:

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