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