proposition: Lemma map_filter_empty_iff m : filter P m = ∅ ↔ map_Forall (λ i x, ¬P (i,x)) m.
proof: Proof. rewrite map_empty. setoid_rewrite map_lookup_filter_None. split. - intros Hm i x Hi. destruct (Hm i); naive_solver. - intros Hm i. destruct (m !! i) as [x|] eqn:?; [|by auto]. right; intros ? [= <-]. by apply Hm. Qed.
imports: Coq(Permutation) stdpp(options)