proposition: Theorem fold_left_f_eq : forall (A B : Type)(f1 f2 : A -> B -> A)(ls : list B) a, (forall b, In b ls -> (forall a, (f1 a b) = (f2 a b))) -> fold_left f1 ls a = fold_left f2 ls a.
proof: Proof. induction ls; intuition idtac; simpl in *. rewrite H. eapply IHls. intuition idtac. eauto. intuition idtac. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation