proposition: Lemma split_spec1 : forall s x y `{Ok s}, (InT y (split x s)#l <-> InT y s /\ X.lt y x).
proof: Proof. induct s x. - intuition_in. - intuition_in; order. - specialize (IHl x y). destruct (split x l); simpl in *. rewrite IHl; intuition_in; order. - specialize (IHr x y). destruct (split x r); simpl in *. rewrite join_spec, IHr; intuition_in; order. Qed.
imports: FunInd MSetInterface MSetGenTree BinInt Int