fact: Fixpoint del x t := match t with | Leaf => Leaf | Node _ a y b => match X.compare x y with | Eq => append a b | Lt => match a with | Bk _ _ _ => lbalS (del x a) y b | _ => Rd (del x a) y b end | Gt => match b with | Bk _ _ _ => rbalS a y (del x b) | _ => Rd a y (del x b) end end end.
imports: Bool List BinPos Pnat Setoid SetoidList PeanoNat