proposition: Lemma sumList_permutation : forall (A : Set)(f : A -> Rat) ls1 ls2, Permutation ls1 ls2 -> sumList ls1 f == sumList ls2 f.
proof: Proof. intuition. eapply fold_add_permutation; intuition. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation