Nuprl - Proof: num iso 2 2 2 1

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

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''
6. x'>x''

x' = x''

By:	SwapEquands 0 THEN BackThru 4 THEN StrongAuto THEN Try (Complete (Unfold `label` 0))

Generated subgoals:

None

About:

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