proposition: Lemma bindings_node_acc (t1 t2:t elt) x e z acc : bindings (Node z t1 x e t2) ++ acc = bindings t1 ++ (x,e) :: bindings t2 ++ acc.
proof: Proof. unfold bindings; simpl; intros. rewrite !bindings_app, !app_nil_r, <- !app_assoc; auto. Qed.
imports: Coq(Bool Arith BinInt FunInd) Coq(Orders OrdersFacts OrdersLists) MMaps(Comparisons Interface OrdList)