'a,'b:S.
Thm* and
Thm* (all(
a:hsum('a; 'b). equal(abs_sum(rep_sum(a)),a))
Thm* ,all
Thm* ,(
r:hbool 
'a 'b hbool. equal
Thm* ,(
r:hbool 'a 'b hbool. (is_sum_rep(r)
Thm* ,(
r:hbool 'a 'b hbool. ,equal(rep_sum(abs_sum(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,'b:S. 'a'b 
ST:S, P,Q:(TType). (x:T. P(x) 
Q(x)) (@x:T. P(x)) = (@x:T. Q(x))