proposition: Lemma map_2_mid: forall {A B: Type} (f: A -> B) l x1 x2 l1 l2 l3, map f l = l1 ++ x1 :: l2 ++ x2 :: l3 -> exists y1 y2 m1 m2 m3, l = m1 ++ y1 :: m2 ++ y2 :: m3 /\ map f m1 = l1 /\ map f m2 = l2 /\ map f m3 = l3 /\ f y1 = x1 /\ f y2 = x2.
proof: Proof. intros. apply map_mid in H. destruct H as [y1 [m1 [m4 [? [? [? ?]]]]]]. apply map_mid in H2. destruct H2 as [y2 [m2 [m3 [? [? [? ?]]]]]]. subst m4. exists y1, y2, m1, m2, m3. 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