proposition: Lemma bindings_spec2 m : sort lt_key (bindings m).
proof: Proof. unfold bindings. apply xbindings_sort. constructor. inversion 2. Qed.
imports: Coq(Bool PeanoNat BinPos Orders OrdersEx OrdersLists) MMaps(Utils Comparisons Interface)