proposition: Lemma In_NoDup_Permutation A (a : A) l (IN: In a l) (ND : NoDup l) : exists l', Permutation l (a :: l') /\ ~ In a l'.
proof: Proof. induction l; ins; desf; inv ND; eauto. destruct IHl as (l' & ? & ?); eauto. destruct (classic (a0 = a)); desf. eexists (a0 :: l'); split; try red; ins; desf. eapply Permutation_trans, perm_swap; eauto. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation