proposition: Lemma set_fold_comm_acc (f : A → A → A) (g : A → A) (a : A) X : (∀ x y, f x (g y) = g (f x y)) → set_fold f (g a) X = g (set_fold f a X).
proof: Proof. intros. apply (set_fold_comm_acc_strong _); [solve_proper|auto]. Qed.
imports: stdpp(relations) stdpp(options)