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