proposition: Lemma list_map_DoubleNoDup_incl_eq: forall l1 l2 v, DoubleNoDup (l2 ++ l1) -> (In v (map fst (l2 ++ l1)) -> In v (map fst l1)) -> 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)). 2: now apply H0 in i. rewrite In_map_fst_iff in i0. destruct i0 as [b ?]. rewrite !(list_map_In _ _ b); auto. + now apply DoubleNoDup_fst in H. + rewrite in_app_iff. now right. + rewrite DoubleNoDup_app_iff in H. destruct H as [? [? ?]]. now apply DoubleNoDup_fst in H2. - 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