proposition: Lemma Permutation_spec_Prop_join: forall {A : Type} (l : list A) (P Pf: A -> Prop) (x : A), Prop_join (eq x) Pf P -> (forall y : A, In y l <-> P y) /\ NoDup l -> (exists l', Permutation l (x :: l') /\ (forall y : A, In y l' <-> Pf y) /\ NoDup l').
proof: Proof. intros. destruct H, H0. assert (In x l) by (rewrite H0, H; auto). destruct (In_Permutation_cons _ _ H3) as [l' ?]. exists l'. split; auto. pose proof Permutation_NoDup H4 H2. pose proof NoDup_cons_1 _ _ _ H5. pose proof NoDup_cons_2 _ _ _ H5. split; auto. intros. pose proof @Permutation_in _ _ _ y H4. pose proof @Permutation_in _ _ _ y (Permutation_sym H4). simpl in H8, H9. clear H6 H2 H3 H4 H5. specialize (H y). specialize (H0 y). specialize (H1 y). assert (x = y -> ~ In y l') by (intros; subst; auto). 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