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