Lemma foldMapAdd : forall (A : Type) (vs : list A) (f : A -> nat),
  fold_right (fun v acc => f v + acc) 0 vs = fold_right (fun x y => x + y) 0 (map f vs).
Proof.
  (** Proof omitted for brevity. *)
Qed.
