diff --git a/theories/program_logic/total_adequacy.v b/theories/program_logic/total_adequacy.v
index c3d0235b91274b3967dca1a843876a920943ff32..774dbf1d7ed7c8b96c1197f3d2d929af98391fa2 100644
--- a/theories/program_logic/total_adequacy.v
+++ b/theories/program_logic/total_adequacy.v
@@ -51,7 +51,7 @@ Proof.
   iIntros (t1 t1' Ht) "Ht1". iRevert (t1' Ht); iRevert (t1) "Ht1".
   iApply twptp_ind; iIntros "!>" (t1) "IH"; iIntros (t1' Ht).
   rewrite twptp_unfold /twptp_pre. iIntros (t2 σ1 κ κs σ2 n Hstep) "Hσ".
-  destruct (step_Permutation t1' t1 t2 κ σ1 σ2) as (t2'&?&?); try done.
+  destruct (step_Permutation t1' t1 t2 κ σ1 σ2) as (t2'&?&?); [done..|].
   iMod ("IH" $! t2' with "[% //] Hσ") as (n2) "($ & Hσ & IH & _)".
   iModIntro. iExists n2. iFrame "Hσ". by iApply "IH".
 Qed.