proposition: Lemma map_to_list_delete {A} (m : M A) i x : m !! i = Some x → (i,x) :: map_to_list (delete i m) ≡ₚ map_to_list m.
proof: Proof. intros. rewrite <-map_to_list_insert by (by rewrite lookup_delete). by rewrite insert_delete. Qed.
imports: Coq(Permutation) stdpp(options)