proposition: Lemma map_lookup_filter_Some m i x : filter P m !! i = Some x ↔ m !! i = Some x ∧ P (i, x).
proof: Proof. rewrite map_lookup_filter. destruct (m !! i); simpl; repeat case_guard; naive_solver. Qed.
imports: Coq(Permutation) stdpp(options)