diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 67b242f3a3ad93e14c6af2c626e58b61da0a8673..7185a59fafaeac1ad9f0a7b0377fd19fc74019e6 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -1119,6 +1119,8 @@ Proof.
   naive_solver eauto using map_Forall_insert_11,
     map_Forall_insert_12, map_Forall_insert_2.
 Qed.
+Lemma map_Forall_delete m i : map_Forall P m → map_Forall P (delete i m).
+Proof. intros Hm j x; rewrite lookup_delete_Some. naive_solver. Qed.
 Lemma map_Forall_ind (Q : M A → Prop) :
   Q ∅ →
   (∀ m i x, m !! i = None → P i x → map_Forall P m → Q m → Q (<[i:=x]>m)) →