proposition: Theorem fold_left_invol: forall (f: A -> B -> A) (P: A -> Prop) l a, P a -> (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. Qed.
imports: List Arith Tactic Inverse_Image Wf_nat