rep:hnum 
hind. type_definition(is_num_rep,rep))
'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)| Theorem | Name |
| rep:hnum hind. type_definition(is_num_rep,rep)) | [hnum_ty_def] |
| cites the following: | |
| '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')) | [type_def_iso] |
| ;;is_num_rep;rep_num;abs_num) | [num_iso] |