proposition: Theorem fold_left_init : (forall (a : A) (b : B), h (f a b) = f (h a) b) -> forall (a : A) (l : list B), fold_left f l (h a) = h (fold_left f l a).
proof: Proof. intros H a l; generalize a; elim l; clear l a; simpl in |- *; auto. intros a l H0 a0. rewrite <- H; auto. Qed.
imports: Coq(Inverse_Image Wf_nat Sorting.Permutation)