proposition: Theorem fold_left_comm_perm_eq : forall (A B : Type)(ls1 ls2 : list B), Permutation ls1 ls2 -> forall (f : A -> B -> A) init, (forall a b1 b2, f (f a b1) b2 = f (f a b2) b1) -> fold_left f ls1 init = fold_left f ls2 init.
proof: Proof. induction 1; intuition idtac. simpl. eauto. simpl. rewrite H. eauto. rewrite IHPermutation1. apply IHPermutation2. intuition idtac. intuition idtac. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation