proposition: Lemma map_filter_fmap {B} (f : B → A) (m : M B) : filter P (f <$> m) = f <$> filter (λ '(i, x), P (i, (f x))) m.
proof: Proof. apply map_eq. intros i. apply option_eq; intros x. repeat (rewrite lookup_fmap, fmap_Some || setoid_rewrite map_lookup_filter_Some). naive_solver. Qed.
imports: Coq(Permutation) stdpp(options)