proposition: Lemma remove_NoDup : forall m (Hm:NoDupA m) x, NoDupA (remove x m).
proof: Proof. induction m. - simpl; intuition. - intros. inversion_clear Hm. destruct a as (x',e'). simpl; case (X.eq_dec x x'); auto. constructor; auto. contradict H; apply remove_3' with x; auto. Qed.
imports: FMapInterface