proposition: Lemma gmultiset_set_fold_comm_acc (f : A → A → A) (g : A → A) (a : A) X : (∀ x c, g (f x c) = f x (g c)) → set_fold f (g a) X = g (set_fold f a X).
proof: Proof. intros. apply (gmultiset_set_fold_comm_acc_strong _); [solve_proper|done]. Qed.
imports: stdpp(gmap) stdpp(options)