Nuprl - Proof: hzero def 1 2

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

a,r:

.
1. iso_pair(

;

;is_num_rep;rep_num;abs_num)

rep_num(a) = r

a = abs_num(r)

rep_num(0) = zero_rep

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

Generated subgoals:

None

About:

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