proposition: Lemma create_spec : forall l x r y, InT y (create l x r) <-> X.eq y x \/ InT y l \/ InT y r.
proof: Proof. unfold create; split; [ inversion_clear 1 | ]; intuition. Qed.
imports: FunInd MSetInterface MSetGenTree BinInt Int