Nuprl - Proof: num iso 4 2

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

1. x :

x':

. x = rep_num(x')
3.

. is_num_rep(rep_num(m))

is_num_rep(x)

By:	Analyze 2 THEN StrongAuto THEN Try (Complete (Unfold `label` 0))

Generated subgoal:

1 2. x' :
3. x = rep_num(x')
4. m:. is_num_rep(rep_num(m))
is_num_rep(x)
1 step

About:

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