proposition: Lemma rev_bindings_aux_rev m acc : rev_bindings_aux acc m = rev (bindings m) ++ acc.
proof: Proof. revert acc. induction m; simpl; intros; auto. rewrite IHm2, IHm1, bindings_node, !rev_app_distr. simpl. now rewrite <- !app_assoc. Qed.
imports: Coq(Bool Arith BinInt FunInd) Coq(Orders OrdersFacts OrdersLists) MMaps(Comparisons Interface OrdList)