proposition: Theorem singleton_spec i x : bindings (singleton i x) = (i,x)::nil.
proof: Proof. unfold singleton. induction i; simpl; auto. - now rewrite bindings_node; simpl; rewrite IHi. - now rewrite bindings_node; simpl; rewrite IHi. Qed.
imports: Coq(Bool PeanoNat BinPos Orders OrdersEx OrdersLists) MMaps(Utils Comparisons Interface)