proposition: Lemma foldr_delete_intersection_with (m1 m2 : M A) is : foldr delete (intersection_with f m1 m2) is = intersection_with f (foldr delete m1 is) (foldr delete m2 is).
proof: Proof. induction is as [|?? IHis]; simpl; [done|]. by rewrite IHis, delete_intersection_with. Qed.
imports: Coq(Permutation) stdpp(options)