proposition: Lemma remove_in : forall m x y, bst m -> (In y (remove x m) <-> ~ X.eq y x /\ In y m).
proof: Proof. intros m x; functional induction (remove x m); simpl; intros. - intuition_in. - inv bst; clear e0. rewrite bal_in; auto. generalize (IHt y0 H0); intuition; [ order | order | intuition_in ]. - inv bst; clear e0. rewrite merge_in; intuition; [ order | order | intuition_in ]. elim H4; eauto with ordered_type. - inv bst; clear e0. rewrite bal_in; auto. generalize (IHt y0 H1); intuition; [ order | order | intuition_in ]. Qed.
imports: FunInd FMapInterface FMapList ZArith Int