proposition: Lemma map_Exists_delete m i : map_Exists P (delete i m) → map_Exists P m.
proof: Proof. intros [j [y [Hm ?]]]. rewrite lookup_delete_Some in Hm. unfold map_Exists. naive_solver. Qed.
imports: Coq(Permutation) stdpp(options)