proposition: Lemma split_ok : forall s x `{Ok s}, Ok (split x s)#l /\ Ok (split x s)#r.
proof: Proof. induct s x; simpl; auto. - specialize (IHl x). generalize (fun y => @split_spec2 l x y _). destruct (split x l); simpl in *; intuition. apply join_ok; auto. intros y; rewrite H; intuition. - specialize (IHr x). generalize (fun y => @split_spec1 r x y _). destruct (split x r); simpl in *; intuition. apply join_ok; auto. intros y; rewrite H; intuition. Qed.
imports: FunInd MSetInterface MSetGenTree BinInt Int