diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index cd4b760209e71798be20077b45ffa79a17f3590e..625970eee44ebcdd6e1004ede6e9e8cbdeb3cf20 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -122,6 +122,10 @@ Tactic Notation "iAssumptionCore" :=
      first [is_evar i; fail 1 | env_cbv; reflexivity]
   | |- envs_lookup ?i (Envs ?Γp ?Γs) = Some (_, ?P) =>
      is_evar i; first [find Γp i P | find Γs i P]; env_cbv; reflexivity
+  | |- envs_lookup_delete ?i (Envs ?Γp ?Γs) = Some (_, ?P, _) =>
+     first [is_evar i; fail 1 | env_cbv; reflexivity]
+  | |- envs_lookup_delete ?i (Envs ?Γp ?Γs) = Some (_, ?P, _) =>
+     is_evar i; first [find Γp i P | find Γs i P]; env_cbv; reflexivity
   end.
 
 Tactic Notation "iAssumption" :=