proposition: Lemma bindings_spec2 m `{!Ok m} : sort ltk (bindings m).
proof: Proof. unfold bindings; apply bindings_aux_sort; auto. inversion 1. Qed.
imports: Coq(Bool Arith BinInt FunInd) Coq(Orders OrdersFacts OrdersLists) MMaps(Comparisons Interface OrdList)