fact: Fixpoint cons s e : enumeration := match s with | Leaf => e | Node _ l x v r => cons l (More x v r e) end.
imports: Coq(Bool Arith BinInt FunInd) Coq(Orders OrdersFacts OrdersLists) MMaps(Comparisons Interface OrdList)