proposition: Theorem fold_left_map : forall (C : Type) a l (k : C -> B), fold_left f (map k l) a = fold_left (fun a b => f a (k b)) l a.
proof: Proof. intros C a l k; generalize a; elim l; simpl in |- *; auto. Qed.
imports: Coq(Inverse_Image Wf_nat Sorting.Permutation)