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