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