proposition: Lemma bindings_3w m : NoDupA eq_key (bindings m).
proof: Proof. apply bindings_spec2w. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)