proposition: Lemma map_filter_insert m i x : filter P (<[i:=x]> m) = if decide (P (i, x)) then <[i:=x]> (filter P m) else filter P (delete i m).
proof: Proof. apply map_eq. intros j. apply option_eq; intros y. rewrite map_lookup_filter_Some, lookup_insert_Some. case_decide. - rewrite lookup_insert_Some, map_lookup_filter_Some. naive_solver. - rewrite map_lookup_filter_Some, lookup_delete_Some. naive_solver. Qed.
imports: Coq(Permutation) stdpp(options)