proposition: Lemma find_1 : forall m (Hm:NoDupA m) x e, MapsTo x e m -> find x m = Some e.
proof: Proof. intros m; induction m as [|[a e]]; simpl; intros Hdup x e' Hm. - inversion Hm. - inversion_clear Hdup. inversion_clear Hm; destruct X.eq_dec. + destruct H1; simpl in *; congruence. + elim n; apply H1. + elim H; apply InA_eqk with (x,e'); auto. + apply IHm; auto. Qed.
imports: FMapInterface