proposition: Lemma remove_bst : forall m x, bst m -> bst (remove x m).
proof: Proof. intros m x; functional induction (remove x m); simpl; intros. - auto. - inv bst. apply bal_bst; auto. intro; intro. rewrite (remove_in x y0 H0) in H; auto. destruct H; eauto. - inv bst. apply merge_bst; eauto with ordered_type. - inv bst. apply bal_bst; auto. intro; intro. rewrite (remove_in x y0 H1) in H; auto. destruct H; eauto. Qed.
imports: FunInd FMapInterface FMapList ZArith Int