IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
his num rep wd1 1. m : (is_num_rep(m))
= (P:. ((P(zero_rep))(n:. (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