proposition: Lemma fold_add_init_nat_h : forall (A : Set)(f : A -> nat)(ls : list A)(init1 init2 : nat), (fold_left (fun acc a => acc + (f a))%nat ls (init1 + init2) = init1 + fold_left (fun acc a => acc + (f a))%nat ls init2)%nat.
proof: Proof. induction ls; intuition; simpl in *. rewrite <- Nat.add_assoc. eapply IHls. Qed.
imports: FCF.FCF Permutation