proposition: Lemma map_lookup_filter_None m i : filter P m !! i = None ↔ m !! i = None ∨ ∀ x, m !! i = Some x → ¬ P (i, x).
proof: Proof. rewrite eq_None_not_Some. unfold is_Some. setoid_rewrite map_lookup_filter_Some. naive_solver. Qed.
imports: Coq(Permutation) stdpp(options)