proposition: Theorem list_fold_right_map : ∀ A B C (f : B → A → A) (g : C → B) l a, List.fold_right f a (List.map g l) = List.fold_right (λ b acc, f (g b) acc) a l.
proof: Proof. intros A B C f g l a. induction l as [| x]; [ reflexivity | simpl; f_equal; assumption ]. Qed.
imports: Utf8 QArith NPeano Sorted Psatz