Hi Andreas,
recursive definitions are really hard!
What you try to achieve is too much for me to do in a single go, so I tried something simpler and proved the analogous properties for the function that adds up all elements of a finite set of integers. The result is attached. You'll observe that I strictly followed the sequence of definitions and lemmas from module WellFoundedInduction.
I believe that in order to obtain what you want to achieve one can first do a similar development for bags of integers by iterating over the domain of the bag (which is a set of integers) and add the domain element times its multiplicity. Then extend to bags of pairs of integers by first summing the pair.
Of course I agree that it would be good to have generic lemmas over fold operators, and I will do that when I find some time.
Hope this helps,
Stephan