proposition: Lemma create_bindings l x e r : bindings (create l x e r) = bindings l ++ (x,e) :: bindings r.
proof: Proof. apply bindings_node. Qed.
imports: Coq(Bool PeanoNat BinInt FunInd Int) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)