proposition: Lemma map_mid: forall {A B: Type} (f: A -> B) l x xl1 xl2, map f l = xl1 ++ x :: xl2 -> exists y yl1 yl2, l = yl1 ++ y :: yl2 /\ f y = x /\ map f yl1 = xl1 /\ map f yl2 = xl2.
proof: Proof. intros. revert xl1 H. induction l; intros. 1: simpl in H; destruct xl1; inversion H. destruct xl1. + clear IHl. simpl in H. exists a, nil, l. inversion H. split; auto. + simpl in H. inversion H. specialize (IHl _ H2). destruct IHl as [y [yl1 [yl2 [? [? [? ?]]]]]]. exists y, (a :: yl1), yl2. simpl. subst l. rewrite H4. 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