proposition: Lemma set_fold_proper {B} (R : relation B) `{!PreOrder R} (f : A → B → B) (b : B) `{!∀ a, Proper (R ==> R) (f a)} (Hf : ∀ a1 a2 b, R (f a1 (f a2 b)) (f a2 (f a1 b))) : Proper ((≡) ==> R) (set_fold f b : C → B).
proof: Proof. intros ?? E. apply (foldr_permutation R f b); auto. by rewrite E. Qed.
imports: stdpp(relations) stdpp(options)