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