proposition: Theorem fold_left_invol_in: forall (f: A -> B -> A) (P: A -> Prop) l a b, In b l -> (forall x, P (f x b)) -> (forall x y, P x -> P (f x y)) -> P (fold_left f l a).
proof: Proof. intros f1 P l; elim l; simpl; auto. intros a1 b HH; case HH. intros a1 l1 Rec a2 b [V|V] V1 V2; subst; auto. apply fold_left_invol; auto. apply Rec with (b := b); auto. Qed.
imports: List Arith Tactic Inverse_Image Wf_nat