Nuprl - Proof: hnum ty def 1

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

rep:(hnum

hind). type_definition(hind;hnum;is_num_rep;rep)

By:	Inst Thm* 'a,'b:S, P:('b), rep:('a'b), abs:('b'a). Thm* iso_pair('a;'b;P;rep;abs) Thm* Thm* (rep':('a'b). type_definition('b;'a;P;rep')) [;;is_num_rep;rep_num;abs_num] THEN StrongAuto

Generated subgoal:

1 iso_pair(;;is_num_rep;rep_num;abs_num)
1 step

About:

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