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