proposition: Lemma map_to_list_insert {A} (m : M A) i x : m !! i = None → map_to_list (<[i:=x]>m) ≡ₚ (i,x) :: map_to_list m.
proof: Proof. intros. apply list_to_map_inj; csimpl. - apply NoDup_fst_map_to_list. - constructor; [|by auto using NoDup_fst_map_to_list]. rewrite elem_of_list_fmap. intros [[??] [? Hlookup]]; subst; simpl in *. rewrite elem_of_map_to_list in Hlookup. congruence. - by rewrite !list_to_map_to_list. Qed.
imports: Coq(Permutation) stdpp(options)