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