proposition: Lemma removeA_NoDupA : forall s x, NoDupA s -> NoDupA (removeA x s).
proof: Proof. intros s; induction s as [|a s IHs]; simpl; intros x ?. - auto. - inv. destruct (eqA_dec x a); simpl; auto. constructor; auto. rewrite removeA_InA. intuition. Qed.
imports: List Sorted Setoid Basics Morphisms