proposition: Lemma lbalS_spec l x r y : InT y (lbalS l x r) <-> X.eq y x \/ InT y l \/ InT y r.
proof: Proof. case lbalS_match. - intros; autorew; intuition_in. - clear l. intros l _. destruct r as [|[|] rl rx rr]. * autorew. intuition_in. * destree rl; autorew; intuition_in. * autorew. intuition_in. Qed.
imports: Bool List BinPos Pnat Setoid SetoidList PeanoNat