proposition: Lemma map_filter_insert_not' m i x : ¬ P (i, x) → (∀ y, m !! i = Some y → ¬ P (i, y)) → filter P (<[i:=x]> m) = filter P m.
proof: Proof. intros. rewrite map_filter_insert, decide_False by done. by rewrite map_filter_delete_not. Qed.
imports: Coq(Permutation) stdpp(options)