proposition: Lemma add_1 : forall m x y e, X.eq x y -> MapsTo y e (add x e m).
proof: Proof. intros m x y e; generalize y; clear y. unfold PX.MapsTo. induction m as [|[y e'] m IHm]; simpl. - auto with ordered_type. - intros; destruct X.compare; auto with ordered_type. Qed.
imports: FMapInterface