Nuprl - Proof: hsuc def 1 1

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

a,r:

.
2. iso_pair(

;

;is_num_rep;rep_num;abs_num)

rep_num(a) = r

a = abs_num(r)

iso_pair(

;

;is_num_rep;rep_num;abs_num)

By:	L Thm* iso_pair(;;is_num_rep;rep_num;abs_num) THEN StrongAuto

Generated subgoals:

None

About:

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