proposition: Lemma partial_alter_ext {A} (f g : option A → option A) (m : M A) i : (∀ x, m !! i = x → f x = g x) → partial_alter f i m = partial_alter g i m.
proof: Proof. intros. apply map_eq; intros j. by destruct (decide (i = j)) as [->|?]; rewrite ?lookup_partial_alter, ?lookup_partial_alter_ne; auto. Qed.
imports: Coq(Permutation) stdpp(options)