proposition: Lemma alter_ext {A} (f g : A → A) (m : M A) i : (∀ x, m !! i = Some x → f x = g x) → alter f i m = alter g i m.
proof: Proof. intro. apply partial_alter_ext. intros [x|] ?; f_equal/=; auto. Qed.
imports: Coq(Permutation) stdpp(options)