proposition: Lemma add_2 : forall m x y e e', ~ X.eq x y -> MapsTo y e m -> MapsTo y e (add x e' m).
proof: Proof. induction m as [|[a m]]; intros x y e e' H Hm; simpl in *. - inversion_clear Hm. - inversion_clear Hm; destruct X.eq_dec. + elim H; apply X.eq_trans with a; [auto|apply X.eq_sym; apply H0]. + apply InA_cons_hd; apply H0. + apply InA_cons_tl; assumption. + apply InA_cons_tl; apply IHm; auto. Qed.
imports: FMapInterface