proposition: Theorem fold_left_eta : forall l a f1, (forall a b, In b l -> f a b = f1 a b) -> fold_left f l a = fold_left f1 l a.
proof: Proof. intros l; elim l; simpl in |- *; auto. intros a l0 H a0 f1 H0. rewrite H0; auto. Qed.
imports: Coq(Inverse_Image Wf_nat Sorting.Permutation)