proposition: Lemma map_to_list_to_map {A} (l : list (K * A)) : NoDup (l.*1) → map_to_list (list_to_map l) ≡ₚ l.
proof: Proof. auto using list_to_map_inj, NoDup_fst_map_to_list, list_to_map_to_list. Qed.
imports: Coq(Permutation) stdpp(options)