proposition: Lemma list_to_map_proper {A} (l1 l2 : list (K * A)) : NoDup (l1.*1) → l1 ≡ₚ l2 → (list_to_map l1 : M A) = list_to_map l2.
proof: Proof. intros ? Hperm. apply map_eq. intros i. apply option_eq. intros x. by rewrite <-!elem_of_list_to_map; rewrite <-?Hperm. Qed.
imports: Coq(Permutation) stdpp(options)