proposition: Lemma del_spec : forall s x y `{Ok s}, InT y (del x s) <-> InT y s /\ ~X.eq y x.
proof: Proof. induct s x. - intuition_in. - autorew; intuition_in. + assert (X.lt y x') by eauto. order. + assert (X.lt x' y) by eauto. order. + order. - destruct l as [|[|] ll lx lr]; autorew; rewrite ?IHl by trivial; intuition_in; order. - destruct r as [|[|] rl rx rr]; autorew; rewrite ?IHr by trivial; intuition_in; order. Qed.
imports: Bool List BinPos Pnat Setoid SetoidList PeanoNat