proposition: Lemma sumList_rel_func : forall (A : Set)(f : A -> Rat -> Prop) ls r1, sumList_rel f ls r1 -> forall r2, sumList_rel f ls r2 -> (forall a v1 v2, f a v1 -> f a v2 -> v1 == v2) -> r1 == r2.
proof: Proof. induction 1; intuition. inversion H0; clear H0; subst. rewrite H. rewrite H2. intuition. inversion H2; clear H2; subst. rewrite H1. rewrite H9. eapply ratAdd_eqRat_compat; eauto. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation