proposition: Lemma fold_congruence : forall A B (m:monoid_op B) (f g:A -> B) (E:set A), Comm_monoid m -> finite E -> (forall x, x \in E -> f x = g x) -> fold m f E = fold m g E.
proof: Proof. Proof using. introv Hm HE h. do 2 rewrite fold_eq_fold_to_list. eapply LibList.fold_congruence. intros. eapply h. rewrite finite_eq_in_iff_mem_to_list in HE. rewrite* HE. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibList LibOperation LibMonoid LibInt LibNat LibEpsilon LibRelation LibMin)