proposition: Theorem fold_add_eqRat_compat : forall (A : Set)(ls : list A) f1 f2 init1 init2, (forall r1 r2 a, r1 == r2 -> f1 r1 a == f2 r2 a) -> init1 == init2 -> fold_left f1 ls init1 == fold_left f2 ls init2.
proof: Proof. induction ls; intuition idtac; simpl in *. eapply IHls; intuition idtac. eauto. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation