proposition: Lemma partial_alter_merge g g1 g2 (m1 : M A) (m2 : M B) i : g (diag_None f (m1 !! i) (m2 !! i)) = diag_None f (g1 (m1 !! i)) (g2 (m2 !! i)) → partial_alter g i (merge f m1 m2) = merge f (partial_alter g1 i m1) (partial_alter g2 i m2).
proof: Proof. intro. apply map_eq. intros j. destruct (decide (i = j)); subst. - by rewrite lookup_merge, !lookup_partial_alter, !lookup_merge. - by rewrite lookup_merge, !lookup_partial_alter_ne, lookup_merge. Qed.
imports: Coq(Permutation) stdpp(options)