proposition: Lemma add_not_eq : forall m (Hm:NoDupA m) x a e, ~X.eq x a -> find x (add a e m) = find x m.
proof: Proof. intros. case_eq (find x m); intros. - apply find_1; auto. + apply add_NoDup; auto. + apply add_2; auto. apply find_2; auto. - case_eq (find x (add a e m)); intros; auto. rewrite <- H0; symmetry. apply find_1; auto. apply add_3 with a e; auto. apply find_2; auto. Qed.
imports: FMapInterface