proposition: Lemma filter_2_cons: forall {A: Type} (f: A -> bool) l x1 x2 xl, filter f l = x1 :: x2 :: xl -> exists l1 l2 l3, l = l1 ++ x1 :: l2 ++ x2 :: l3 /\ filter f l1 = nil /\ filter f l2 = nil /\ filter f l3 = xl /\ f x1 = true /\ f x2 = true.
proof: Proof. intros. apply filter_cons in H. destruct H as [l1 [l4 [? [? [? ?]]]]]. apply filter_cons in H1. destruct H1 as [l2 [l3 [? [? [? ?]]]]]. subst l4. exists l1, l2, l3. split; 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