proposition: Lemma list_to_map_flip {A} (m1 : M A) l2 : map_to_list m1 ≡ₚ l2 → m1 = list_to_map l2.
proof: Proof. intros. rewrite <-(list_to_map_to_list m1). auto using list_to_map_proper, NoDup_fst_map_to_list. Qed.
imports: Coq(Permutation) stdpp(options)