proposition: Lemma fold_pointwise : forall B m (leB : B -> B -> Prop), Monoid m -> refl leB -> Proper (leB ++> leB ++> leB) (monoid_oper m) -> forall A (l : list A), forall (f f' : A -> B), (forall x, mem x l -> leB (f x) (f' x)) -> leB (fold m f l) (fold m f' l).
proof: Proof. Proof using. #[global] Hint Constructors mem. introv HM HR HP. induction l; introv HL. do 2 rewrite fold_nil. applys HR. do 2 rewrite fold_cons. apply HP. applys~ HL. applys~ IHl. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)