proposition: Theorem fold_left_init_eq : forall (A : Set)(ls : list A) f init1 init2, (forall a1 a2 b, a1 == a2 -> f a1 b == f a2 b) -> init1 == init2 -> fold_left f ls init1 == fold_left f ls init2.
proof: Proof. induction ls; intuition idtac; simpl in *. apply IHls; intuition. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation