proposition: Lemma fold_congruence : forall m f g l, (forall x, mem x l -> f x = g x) -> fold m f l = fold m g l.
proof: Proof. Proof using. Hint Constructors mem. intros. unfold fold. induction l as [| x l' ]; intros; simpl. { eauto. } { rew_listx. fequals. applys~ H. eauto. } Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)