proposition: Lemma set_fold_disj_union (f : A → A → A) (b : A) X Y : Comm (=) f → Assoc (=) f → X ## Y → set_fold f b (X ∪ Y) = set_fold f (set_fold f b X) Y.
proof: Proof. intros. apply (set_fold_disj_union_strong _ _ _ _ _ _); [|done]. intros x1 x2 b' _ _ _. by rewrite !(assoc_L f), (comm_L f x1). Qed.
imports: stdpp(relations) stdpp(options)