proposition: Lemma map_filter_empty_not_lookup m i x : filter P m = ∅ → P (i,x) → m !! i ≠ Some x.
proof: Proof. rewrite map_empty. setoid_rewrite map_lookup_filter_None. intros Hm ?. destruct (Hm i); naive_solver. Qed.
imports: Coq(Permutation) stdpp(options)