proposition: Lemma insert_union_with_r m1 m2 i x : m1 !! i = None → <[i:=x]>(union_with f m1 m2) = union_with f m1 (<[i:=x]>m2).
proof: Proof. intros Hm1. unfold union_with, map_union_with. by erewrite insert_merge_r by (by rewrite Hm1). Qed.
imports: Coq(Permutation) stdpp(options)