'a,'b:S, u,v:'a+'b. rep_sum(u) = rep_sum(v) 
'a'b 
u = v'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))))