proposition: Lemma alter_id {A} (f : A → A) (m : M A) i : (∀ x, m !! i = Some x → f x = x) → alter f i m = m.
proof: Proof. intros Hi; apply map_eq; intros j; destruct (decide (i = j)) as [->|?]. { rewrite lookup_alter; destruct (m !! j); f_equal/=; auto. } by rewrite lookup_alter_ne by done. Qed.
imports: Coq(Permutation) stdpp(options)