proposition: Lemma sumList_rel_body_eq : forall (A : Type)(rel1 rel2 : A -> Rat -> Prop)(ls1 : list A) r1, sumList_rel rel1 ls1 r1 -> forall ls2 r2, (forall a r', rel1 a r' -> rel2 a r') -> r1 == r2 -> ls1 = ls2 -> sumList_rel rel2 ls2 r2.
proof: Proof. induction 1; intuition; subst. econstructor. rewrite <- H1. trivial. econstructor. eapply IHsumList_rel. intuition. eapply eqRat_refl. trivial. eauto. rewrite <- H3. trivial. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation