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; functional induction (add x e m); intros; inv bst; try rewrite bal_mapsto; unfold create; eauto with ordered_type. Qed.
imports: FunInd FMapInterface FMapList ZArith Int