diff --git a/iris/proofmode/coq_tactics.v b/iris/proofmode/coq_tactics.v
index 3be114662a8f95836da8e865485ab0d87915dc3b..0451e6559912ea8a290ea25172a964ac51598726 100644
--- a/iris/proofmode/coq_tactics.v
+++ b/iris/proofmode/coq_tactics.v
@@ -539,7 +539,7 @@ Lemma tac_pose_proof_hyp Δ i j Q :
 Proof.
   destruct (envs_lookup_delete _ _ _) as [((p&P)&Δ')|] eqn:Hlookup; last done.
   destruct (envs_app _ _ _) as [Δ''|] eqn:?; last done.
-  rewrite envs_entails_eq. rewrite envs_lookup_delete_Some in Hlookup *.
+  rewrite envs_entails_eq. move: Hlookup. rewrite envs_lookup_delete_Some.
   intros [? ->] <-.
   rewrite envs_lookup_sound' // envs_app_singleton_sound //=.
   by rewrite wand_elim_r.