proposition: Lemma split_spec3 : forall s x `{Ok s}, ((split x s)#b = true <-> InT x s).
proof: Proof. induct s x. - intuition_in; try discriminate. - intuition. - specialize (IHl x). destruct (split x l); simpl in *. rewrite IHl; intuition_in; order. - specialize (IHr x). destruct (split x r); simpl in *. rewrite IHr; intuition_in; order. Qed.
imports: FunInd MSetInterface MSetGenTree BinInt Int