proposition: Lemma join_spec : forall l x r y, InT y (join l x r) <-> X.eq y x \/ InT y l \/ InT y r.
proof: Proof. join_tac. - simpl. rewrite add_spec'; intuition_in. - rewrite add_spec'; intuition_in. - rewrite bal_spec, Hlr; clear Hlr Hrl; intuition_in. - rewrite bal_spec, Hrl; clear Hlr Hrl; intuition_in. - apply create_spec. Qed.
imports: FunInd MSetInterface MSetGenTree BinInt Int