proposition: Lemma foldr_delete_commute {A} (m : M A) is j : delete j (foldr delete m is) = foldr delete (delete j m) is.
proof: Proof. induction is as [|?? IH]; [done| ]. simpl. by rewrite delete_commute, IH. Qed.
imports: Coq(Permutation) stdpp(options)