proposition: Lemma list_map_NoDup_app_eq: forall l1 l2 v, NoDup (map fst (l2 ++ l1)) -> (~ In v (map fst l1) -> In (v, v) l2) -> list_map l1 v = list_map (l2 ++ l1) v.
proof: Proof. intros. destruct (in_dec equiv_dec v (map fst (l2 ++ l1))). - destruct (in_dec equiv_dec v (map fst l1)). + rewrite In_map_fst_iff in i0. destruct i0 as [b ?]. erewrite !list_map_In; eauto. 1: rewrite in_app_iff; now right. rewrite map_app in H. now apply NoDup_app_r in H. + rewrite list_map_not_In; auto. apply H0 in n. erewrite list_map_In; eauto. rewrite in_app_iff. now left. - rewrite !list_map_not_In; auto. intro. apply n. rewrite map_app, in_app_iff. now right. 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