proposition: Lemma alter_union_with_l (g : A → A) m1 m2 i : (∀ x y, m1 !! i = Some x → m2 !! i = Some y → g <$> f x y = f (g x) y) → (∀ y, m1 !! i = None → m2 !! i = Some y → g y = y) → alter g i (union_with f m1 m2) = union_with f (alter g i m1) m2.
proof: Proof. intros. apply partial_alter_merge_l. destruct (m1 !! i) eqn:?, (m2 !! i) eqn:?; f_equal/=; auto. Qed.
imports: Coq(Permutation) stdpp(options)