proposition: Lemma fold_left_map_eq : forall (A B C : Set)(ls : list A)(f1 : A -> B)(f2 : C -> B -> C)(init : C), fold_left (fun acc b => f2 acc b) (map f1 ls) init = fold_left (fun acc a => f2 acc (f1 a)) ls init.
proof: Proof. induction ls; intuition; simpl in *. eauto. Qed.
imports: FCF.FCF Permutation