proposition: Lemma of_list_2 l : NoDupA eqk l -> equivlistA eqke l (to_list (of_list l)).
proof: Proof. intros Hnodup (k,e). rewrite <- bindings_mapsto_iff, of_list_1; intuition. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)