proposition: Lemma gmultiset_set_fold_singleton {B} (f : A → B → B) (b : B) (a : A) : set_fold f b ({[+ a +]} : gmultiset A) = f a b.
proof: Proof. by unfold set_fold; simpl; rewrite gmultiset_elements_singleton. Qed.
imports: stdpp(gmap) stdpp(options)