'a,'b:S.
Thm* (
x:'a+'b. abs_sum(rep_sum(x)) = x 
'a+'b)
Thm* & (
x:(
'a'b). is_sum_rep(x) = ((rep_sum(abs_sum(x))) =
x))'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))))