fact: Fixpoint remove x s := match s with | Leaf => Leaf | Node _ l y r => match X.compare x y with | Lt => bal (remove x l) y r | Eq => merge l r | Gt => bal l y (remove x r) end end.
imports: FunInd MSetInterface MSetGenTree BinInt Int