proposition: Lemma list_to_map_inj {A} (l1 l2 : list (K * A)) : NoDup (l1.*1) → NoDup (l2.*1) → (list_to_map l1 : M A) = list_to_map l2 → l1 ≡ₚ l2.
proof: Proof. intros ?? Hl1l2. apply NoDup_Permutation; [by eauto using NoDup_fmap_1..|]. intros [i x]. by rewrite !elem_of_list_to_map, Hl1l2. Qed.
imports: Coq(Permutation) stdpp(options)