diff --git a/theories/program_logic/adequacy.v b/theories/program_logic/adequacy.v
index b448661ab9c05d8d98891cf58540f05f5c7d0cbd..fdbb25a23294b0708b2f1a72c675da22772141c2 100644
--- a/theories/program_logic/adequacy.v
+++ b/theories/program_logic/adequacy.v
@@ -158,7 +158,7 @@ Proof.
   - iDestruct "Ht" as "(_ & He2 & _)". by iMod (wp_safe with "Hσ He2").
 Qed.
 
-Lemma wptp_invariance φ s n e1 κs κs' e2 t1 t2 σ1 σ2 Φ :
+Lemma wptp_invariance φ s n e1 κs κs' t1 t2 σ1 σ2 Φ :
   nsteps n (e1 :: t1, σ1) κs (t2, σ2) →
   (state_interp σ2 κs' (pred (length t2)) ={⊤,∅}=∗ ⌜φ⌝) -∗
   state_interp σ1 (κs ++ κs') (length t1) -∗