proposition: Theorem sumList_permutation_body_eq: forall (A : Set) (f1 f2 : A -> Rat) (ls1 ls2 : list A), Permutation ls1 ls2 -> (forall a, In a ls2 -> (f1 a == f2 a)) -> sumList ls1 f1 == sumList ls2 f2.
proof: Proof. intros. eapply eqRat_trans. eapply sumList_permutation; eauto. eapply sumList_body_eq; intuition idtac. Qed.
imports: FCF FCF.PRF Permutation