proposition: Lemma bindings_spec2' (m:t elt) : sort ltk (bindings m).
proof: Proof. apply bindings_spec2. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)