diff --git a/program_logic/adequacy.v b/program_logic/adequacy.v
index a6b3dbb892c9b6b817a96bb0782429cd1842c688..688a02079f3b055c43780b1a2dbc7a40f984f0e2 100644
--- a/program_logic/adequacy.v
+++ b/program_logic/adequacy.v
@@ -115,7 +115,7 @@ Lemma wptp_safe n e1 e2 t1 t2 σ1 σ2 Φ :
   world σ1 ★ WP e1 {{ Φ }} ★ wptp t1 ⊢
   Nat.iter (S (S n)) (λ P, |=r=> ▷ P) (■ (is_Some (to_val e2) ∨ reducible e2 σ2)).
 Proof.
-  intros ? He2. rewrite wptp_steps // (Nat_iter_S_r (S n)); apply: rvs_iter_mono.
+  intros ? He2. rewrite wptp_steps //; rewrite (Nat_iter_S_r (S n)). apply rvs_iter_mono.
   iDestruct 1 as (e2' t2') "(% & Hw & H & Htp)"; simplify_eq.
   apply elem_of_cons in He2 as [<-|?]; first (iApply wp_safe; by iFrame "Hw H").
   iApply wp_safe. iFrame "Hw".