Nuprl - Proof: num iso 2 2

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: num iso 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

x' = x''

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

Generated subgoals:

1 5. x'<x''
x' = x''
1 step

2 5. x'<x''
x' = x''
2 steps

About:

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