proposition: Lemma map_filter_alt m : filter P m = list_to_map (filter P (map_to_list m)).
proof: Proof. apply list_to_map_flip. induction m as [|k x m ? IH] using map_ind. { by rewrite map_to_list_empty, map_filter_empty, map_to_list_empty. } rewrite map_to_list_insert, filter_cons by done. destruct (decide (P _)). - rewrite map_filter_insert_True by done. by rewrite map_to_list_insert, IH by (rewrite map_lookup_filter_None; auto). - by rewrite map_filter_insert_not' by naive_solver. Qed.
imports: Coq(Permutation) stdpp(options)