'a,'b:S.
  (x:'a+'b. abs_sum(rep_sum(x)) = x  'a+'b)
  & (x:('a'b). is_sum_rep(x) = ((rep_sum(abs_sum(x))) = x))

None

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html