proposition: Lemma fold_add_nat_0 : forall (A : Set)(ls : list A)(f : A -> nat), (forall a, In a ls -> f a = O) -> fold_left (fun acc a => acc + (f a))%nat ls O = O.
proof: Proof. induction ls; intuition; simpl in *. rewrite H; intuition. Qed.
imports: FCF.FCF Permutation