proposition: Lemma list_to_map_snoc {A} (l : list (K * A)) i x : i ∉ l.*1 → list_to_map (l ++ [(i, x)]) =@{M A} <[i:=x]>(list_to_map l).
proof: Proof. induction l as [|[k y] l IH]; [done|]. csimpl. intros [Hneq Hni]%not_elem_of_cons. by rewrite (IH Hni), insert_commute by done. Qed.
imports: Coq(Permutation) stdpp(options)