proposition: Lemma insert_merge_l (m1 : M A) (m2 : M B) i x y : f (Some y) (m2 !! i) = Some x → <[i:=x]>(merge f m1 m2) = merge f (<[i:=y]>m1) m2.
proof: Proof. by intros; apply partial_alter_merge_l. Qed.
imports: Coq(Permutation) stdpp(options)