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.