proposition: Lemma add_3 : forall m x y e e', ~ X.eq x y -> MapsTo y e (add x e' m) -> MapsTo y e m.
proof: Proof. intros m x y e e' He H; unfold PX.MapsTo in *. induction m as [|[z e''] m IHm]; simpl in *. - apply (In_inv_3 H); auto with ordered_type. - destruct X.compare as [Hlt|Heq|Hgt]; simpl. + apply (In_inv_3 H); auto with ordered_type. + constructor 2; apply (In_inv_3 H); auto with ordered_type. + inversion_clear H; auto. Qed.
imports: FMapInterface