proposition: Lemma add_1 : forall m x y e, X.eq x y -> MapsTo y e (add x e m).
proof: Proof. induction m as [|[a m]]; intros x y e He; simpl in *; auto. destruct X.eq_dec; [now auto|]. apply InA_cons_tl, IHm, He. Qed.
imports: FMapInterface