proposition: Lemma rbalS_spec l x r y : InT y (rbalS l x r) <-> X.eq y x \/ InT y l \/ InT y r.
proof: Proof. case rbalS_match. - intros; autorew; intuition_in. - intros t _. destruct l as [|[|] ll lx lr]. * autorew. intuition_in. * destruct lr as [|[|] lrl lrx lrr]; autorew; intuition_in. * autorew. intuition_in. Qed.
imports: Bool List BinPos Pnat Setoid SetoidList PeanoNat