proposition: Lemma add_spec' : forall s x y, InT y (add x s) <-> X.eq y x \/ InT y s.
proof: Proof. induct s x; try rewrite ?bal_spec, ?IHl, ?IHr; intuition_in. setoid_replace y with x'; eauto. Qed.
imports: FunInd MSetInterface MSetGenTree BinInt Int