proposition: Lemma foldr_delete_insert {A} (m : M A) is j x : j ∈ is → foldr delete (<[j:=x]>m) is = foldr delete m is.
proof: Proof. induction 1 as [i is|j i is ? IH]; simpl; [|by rewrite IH]. by rewrite !foldr_delete_commute, delete_insert_delete. Qed.
imports: Coq(Permutation) stdpp(options)