proposition: Lemma bindings_spec2w m `{!Ok m} : NoDupA eqk (bindings m).
proof: Proof. intros; apply O.Sort_NoDupA; autom. Qed.
imports: Coq(Bool Arith BinInt FunInd) Coq(Orders OrdersFacts OrdersLists) MMaps(Comparisons Interface OrdList)