fact: Fixpoint mem x m : bool := match m with | Leaf => false | Node l y _ r _ => match X.compare x y with | LT _ => mem x l | EQ _ => true | GT _ => mem x r end end.
imports: FunInd FMapInterface FMapList ZArith Int