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. intros m x y e e'; induction m; simpl; auto. destruct (X.compare x k); intros; inv bst; try rewrite bal_mapsto; unfold create; auto; inv MapsTo; auto; order. Qed.
imports: FunInd FMapInterface FMapList ZArith Int