proposition: Lemma singleton_spec x (e:elt) : bindings (singleton x e) = (x,e)::nil.
proof: Proof. unfold singleton. now rewrite bindings_node. Qed.
imports: Coq(Bool PeanoNat BinInt FunInd Int) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)