proposition: Lemma nodup_remove_perm: forall {A : Type} (eq_dec : forall x y : A, {x = y} + {x <> y}) (l : list A) (x : A), NoDup l -> In x l -> Permutation l (x :: remove eq_dec x l).
proof: Proof. intros. apply in_split in H0. destruct H0 as [l1 [l2 ?]]. subst. rewrite (remove_middle eq_dec _ _ _ H). rewrite app_cons_assoc. apply (@Permutation_app_tail _ _ (x :: l1) l2), Permutation_sym, Permutation_cons_append. 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