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