proposition: Lemma filter_cons: forall {A: Type} (f: A -> bool) l x xl, filter f l = x :: xl -> exists l1 l2, l = l1 ++ x :: l2 /\ filter f l1 = nil /\ filter f l2 = xl /\ f x = true.
proof: Proof. intros. induction l. 1: simpl in H; inversion H. simpl in H. destruct (f a) eqn:? . + inversion H. subst a. exists nil, l. split; [|split; [|split]]; auto. + specialize (IHl H). destruct IHl as [l1 [l2 [? [? [? ?]]]]]. exists (a :: l1), l2. split; [|split; [|split]]; auto. - rewrite <- app_comm_cons. subst l. auto. - simpl. destruct (f a) eqn:? . inversion Heqb. auto. Qed.
imports: Coq.Lists.List Coq.micromega.Lia Coq.Sorting.Permutation Coq.ZArith.ZArith_base Coq.ZArith.Zcomplements Coq.Logic.FunctionalExtensionality CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext VST.zlist.sublist VST.zlist.list_solver