proposition: Lemma map_filter_delete m i : filter P (delete i m) = delete i (filter P m).
proof: Proof. apply map_eq. intros j. apply option_eq; intros y. destruct (decide (j = i)) as [->|?]. - rewrite map_lookup_filter_Some, !lookup_delete. naive_solver. - rewrite lookup_delete_ne, !map_lookup_filter_Some, lookup_delete_ne by done. naive_solver. Qed.
imports: Coq(Permutation) stdpp(options)