proposition: Lemma alter_singleton {A} (f : A → A) i x : alter f i {[i := x]} =@{M A} {[i := f x]}.
proof: Proof. intros. apply map_eq. intros i'. destruct (decide (i = i')) as [->|?]. - by rewrite lookup_alter, !lookup_singleton. - by rewrite lookup_alter_ne, !lookup_singleton_ne. Qed.
imports: Coq(Permutation) stdpp(options)