proposition: Lemma gmultiset_set_fold_disj_union (f : A → A → A) (b : A) X Y : Comm (=) f → Assoc (=) f → set_fold f b (X ⊎ Y) = set_fold f (set_fold f b X) Y.
proof: Proof. intros ??; apply gmultiset_set_fold_disj_union_strong; [apply _..|]. intros x1 x2 ? _ _. by rewrite 2!assoc, (comm f x1 x2). Qed.
imports: stdpp(gmap) stdpp(options)