proposition: Lemma fold_left_in_acc_split : forall (A B : Type) (f : A -> list B), let g := fun acc x => (f x) ++ acc in forall acc1 acc2 x l, In x (fold_left g l (acc1 ++ acc2)) <-> In x (fold_left g l acc1) \/ In x acc2.
proof: Proof. intros A B f g acc1 acc2 x l. revert acc1 acc2;induction l as [ | y l]; simpl. split; auto with *. intros acc1 acc2; rewrite <- IHl. unfold g. rewrite ass_app. reflexivity. Qed.
imports: Coq(Bool List Arith Setoid Relations FunInd) CoLoR(closure)