proposition: Lemma gmultiset_set_fold_comm_acc_strong {B} (R : relation B) `{!PreOrder R} (f : A → B → B) (g : B → B) b X : (∀ x, Proper (R ==> R) (f x)) → (∀ x (y : B), x ∈ X → R (f x (g y)) (g (f x y))) → R (set_fold f (g b) X) (g (set_fold f b X)).
proof: Proof. intros ? Hfg. unfold set_fold; simpl. apply foldr_comm_acc_strong; [done|solve_proper|]. intros. by apply Hfg, gmultiset_elem_of_elements. Qed.
imports: stdpp(gmap) stdpp(options)