proposition: Lemma add_NoDup : forall m (Hm:NoDupA m) x e, NoDupA (add x e m).
proof: Proof. induction m. - simpl; constructor; auto; red; inversion 1. - intros. destruct a as (x',e'). simpl; case (X.eq_dec x x'); inversion_clear Hm; auto. + constructor; auto. contradict H. apply InA_eqk with (x,e); auto. + constructor; auto. contradict H; apply add_3' with x e; auto. Qed.
imports: FMapInterface