proposition: Lemma fold_left_in_acc : forall (A B : Type) (f : list B -> A -> list B) x l, (forall acc x y, In y acc -> In x l -> In y (f acc x)) -> forall acc, In x acc -> In x (fold_left f l acc).
proof: Proof. intros A B f x l; induction l as [ | a l]; intros Hf acc x_in_acc; simpl; trivial. apply IHl. intros; apply Hf; [idtac | right]; trivial. apply Hf; [idtac | left]; trivial. Qed.
imports: Coq(Bool List Arith Setoid Relations FunInd) CoLoR(closure)