proposition: Lemma remove_spec : forall s x y `{Ok s}, (InT y (remove x s) <-> InT y s /\ ~ X.eq y x).
proof: Proof. induct s x. - intuition_in. - rewrite merge_spec; intuition; [order|order|intuition_in]. elim H2; eauto. - rewrite bal_spec, IHl; clear IHl IHr; intuition; [order|order|intuition_in]. - rewrite bal_spec, IHr; clear IHl IHr; intuition; [order|order|intuition_in]. Qed.
imports: FunInd MSetInterface MSetGenTree BinInt Int