proposition: Theorem fold_left_permutation : forall (A B : Type) (f : A -> B -> A), (forall (a : A) (b1 b2 : B), f (f a b1) b2 = f (f a b2) b1) -> forall (a : A) (l1 l2 : list B), Permutation l1 l2 -> fold_left f l1 a = fold_left f l2 a.
proof: Proof. intros A B f Hf a l1 l2 H; generalize a; elim H; clear H a l1 l2; simpl in |- *; auto. intros a b l a0; rewrite Hf; auto. intros l1 l2 l3 H H0 H1 H2 a; apply trans_equal with (1 := H0 a); auto. Qed.
imports: Coq(Inverse_Image Wf_nat Sorting.Permutation)