Nuprl - Proof: his num rep wd 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: his num rep wd 1

1. m :

(is_num_rep(m))

(

. ((P(zero_rep))

(

. (P(n))

(P(suc_rep(n)))))

(P(m)))

By:	Unab [`his_num_rep`] THEN Simp THEN StrongAuto

Generated subgoals:

None

About:

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