Thm* (all(
a:hnum. equal(abs_num(rep_num(a)),a))
Thm* ,all(
r:hind. equal(is_num_rep(r),equal(rep_num(abs_num(r)),r))))
;;is_num_rep;rep_num;abs_num)
'a,'b:S, P:('b
), rep:('a'b), abs:('b'a).
Thm* iso_pair('a;'b;P;rep;abs)
Thm*
Thm* (
a:'a. abs(rep(a)) = a) & (r:'b. P(r) = ((rep(abs(r))) =
r))