proposition: Lemma remove_2 : forall m x y e, bst m -> ~X.eq x y -> MapsTo y e m -> MapsTo y e (remove x m).
proof: Proof. intros m x y e; induction m; simpl; auto. destruct (X.compare x k); intros; inv bst; try rewrite bal_mapsto; unfold create; auto; try solve [inv MapsTo; auto]. rewrite merge_mapsto; auto. inv MapsTo; auto; order. Qed.
imports: FunInd FMapInterface FMapList ZArith Int