proposition: Lemma alter_insert {A} (m : M A) i f x : alter f i (<[i := x]> m) = <[i := f x]> m.
proof: Proof. unfold alter, insert, map_alter, map_insert. by rewrite <-partial_alter_compose. Qed.
imports: Coq(Permutation) stdpp(options)