proposition: Lemma 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 b', x1 ∈ X ∪ Y → x2 ∈ X ∪ Y → x1 ≠ x2 → R (f x1 (f x2 b')) (f x2 (f x1 b'))) → X ## Y → R (set_fold f b (X ∪ Y)) (set_fold f (set_fold f b X) Y).
proof: Proof. intros ? Hf Hdisj. unfold set_fold; simpl. rewrite <-foldr_app. apply (foldr_permutation R f b). - intros j1 x1 j2 x2 b' Hj Hj1 Hj2. apply Hf. + apply elem_of_list_lookup_2 in Hj1. set_solver. + apply elem_of_list_lookup_2 in Hj2. set_solver. + intros ->. pose proof (NoDup_elements (X ∪ Y)). by eapply Hj, NoDup_lookup. - by rewrite elements_disj_union, (comm (++)). Qed.
imports: stdpp(relations) stdpp(options)