proposition: Lemma map_to_list_insert_inv {A} (m : M A) l i x : map_to_list m ≡ₚ (i,x) :: l → m = <[i:=x]>(list_to_map l).
proof: Proof. intros Hperm. apply map_to_list_inj. assert (i ∉ l.*1 ∧ NoDup (l.*1)) as []. { rewrite <-NoDup_cons. change (NoDup (((i,x)::l).*1)). rewrite <-Hperm. auto using NoDup_fst_map_to_list. } rewrite Hperm, map_to_list_insert, map_to_list_to_map; auto using not_elem_of_list_to_map_1. Qed.
imports: Coq(Permutation) stdpp(options)