proposition: Lemma map_filter_delete_not m i: (∀ y, m !! i = Some y → ¬ P (i, y)) → filter P (delete i m) = filter P m.
proof: Proof. intros. apply map_filter_strong_ext. intros j y. rewrite lookup_delete_Some. naive_solver. Qed.
imports: Coq(Permutation) stdpp(options)