proposition: Lemma bal_spec : forall l x r y, InT y (bal l x r) <-> X.eq y x \/ InT y l \/ InT y r.
proof: Proof. intros l x r; functional induction bal l x r; intros; try clear e0; rewrite !create_spec; intuition_in. Qed.
imports: FunInd MSetInterface MSetGenTree BinInt Int