proposition: Lemma rev_bindings_rev m : rev_bindings m = rev (bindings m).
proof: Proof. unfold rev_bindings. rewrite rev_bindings_aux_rev. apply app_nil_r. Qed.
imports: Coq(Bool Arith BinInt FunInd) Coq(Orders OrdersFacts OrdersLists) MMaps(Comparisons Interface OrdList)