'a:S.
Thm* and
Thm* (all(
a:hlist('a). equal(abs_list(rep_list(a)),a))
Thm* ,all
Thm* ,(
r:hprod((hnum 
'a); hnum). equal
Thm* ,(
r:hprod((hnum 'a); hnum). (is_list_rep(r)
Thm* ,(
r:hprod((hnum 'a); hnum). ,equal(rep_list(abs_list(r)),r))))'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))'a:S. iso_pair('a List;(
'a)
;is_list_rep;rep_list;abs_list)