proposition: Lemma delete_intersection_with m1 m2 i : delete i (intersection_with f m1 m2) = intersection_with f (delete i m1) (delete i m2).
proof: Proof. by apply (partial_alter_merge _). Qed.
imports: Coq(Permutation) stdpp(options)