Add `set_fold_union_strong` and similarly for map

This discussion at Mattermost nerdsniped me to add the lemma set_fold_union and the stronger lemma set_fold_union_strong that only requires idempotence/associativity/commutativity for the elements in the sets.

Interestingly, the already existing "disjoint" versions of the lemma can be derived.

The proofs are pretty long/tricky, so I tried to add some comments what's going on.