proposition: Lemma NoDupA_swap : forall l l' x, NoDupA (l++x::l') -> NoDupA (x::l++l').
proof: Proof. intros l; induction l as [|a l IHl]; simpl in *; intros l' x H; inv; auto. constructor; eauto. - match goal with H1 : NoDupA (l ++ x :: l') |- _ => assert (H2:=IHl _ _ H1) end. inv. rewrite InA_cons. red; destruct 1. + match goal with H0 : ~ InA a (l ++ x :: l') |- _ => apply H0 end. rewrite InA_app_iff in *; rewrite InA_cons; auto. + auto. - constructor. + match goal with H0 : ~ InA a (l ++ x :: l') |- _ => contradict H0 end. rewrite InA_app_iff in *; rewrite InA_cons; intuition. + eapply NoDupA_split; eauto. Qed.
imports: List Sorted Setoid Basics Morphisms