proposition: Lemma gmultiset_set_fold_disj_union_strong {B} (R : relation B) `{!PreOrder R} (f : A → B → B) (b : B) X Y : (∀ x, Proper (R ==> R) (f x)) → (∀ x1 x2 c, x1 ∈ X ⊎ Y → x2 ∈ X ⊎ Y → R (f x1 (f x2 c)) (f x2 (f x1 c))) → R (set_fold f b (X ⊎ Y)) (set_fold f (set_fold f b X) Y).
proof: Proof. intros ? Hf. unfold set_fold; simpl. rewrite <-foldr_app. apply (foldr_permutation R f b). - intros j1 a1 j2 a2 c ? Ha1%elem_of_list_lookup_2 Ha2%elem_of_list_lookup_2. rewrite gmultiset_elem_of_elements in Ha1, Ha2. eauto. - rewrite (comm (++)). apply gmultiset_elements_disj_union. Qed.
imports: stdpp(gmap) stdpp(options)