proposition: Lemma partial_alter_self_alt {A} (m : M A) i x : x = m !! i → partial_alter (λ _, x) i m = m.
proof: Proof. intros. apply map_eq. intros ii. by destruct (decide (i = ii)) as [->|]; rewrite ?lookup_partial_alter, ?lookup_partial_alter_ne. Qed.
imports: Coq(Permutation) stdpp(options)