fact: Fixpoint mem x t := match t with | Leaf => false | Node _ l k _ r => match K.compare x k with | Lt => mem x l | Eq => true | Gt => mem x r end end.
imports: Coq(Bool Arith BinInt FunInd) Coq(Orders OrdersFacts OrdersLists) MMaps(Comparisons Interface OrdList)