proposition: Lemma sumList_subset' : forall A : Set, eq_dec A -> forall (ls1 ls2 : list A) (f : A -> Rat), NoDup ls1 -> NoDup ls2 -> (forall a : A, In a ls1 -> In a ls2) -> (forall a : A, In a ls2 -> ~ In a ls1 -> f a == 0) -> sumList ls1 f == sumList ls2 f.
proof: Proof. intuition. eapply fold_add_subset'; eauto. intuition. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation