proposition: Lemma NoDupA_split : forall l l' x, NoDupA (l++x::l') -> NoDupA (l++l').
proof: Proof. intros l; induction l; simpl in *; intros; inv; auto. constructor; eauto. match goal with H0 : ~ InA _ _ |- _ => contradict H0 end. rewrite InA_app_iff in *. rewrite InA_cons. intuition. Qed.
imports: List Sorted Setoid Basics Morphisms