proposition: Lemma perm_spec_minus_1: forall {A : Type} (l : list A) (P: A -> Prop) (x : A), P x -> (forall y : A, In y l <-> P y) /\ NoDup l -> (exists l', Permutation l (x :: l') /\ (forall y : A, In y l' <-> P y /\ x <> y) /\ NoDup l').
proof: Proof. intros. destruct H0. rewrite <- H0 in H. destruct (In_Permutation_cons _ _ H) as [l' ?]. exists l'. split; auto. eapply Permutation_NoDup in H1; eauto. pose proof NoDup_cons_1 _ _ _ H1. pose proof NoDup_cons_2 _ _ _ H1. split; [| auto]. intro y; rewrite <- H0. assert (x = y -> ~ In y l') by (intro; subst; auto). pose proof @Permutation_in _ _ _ y H2. pose proof @Permutation_in _ _ _ y (Permutation_sym H2). simpl in H6, H7. tauto. 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