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