diff --git a/theories/hocap/concurrent_runners.v b/theories/hocap/concurrent_runners.v
index 476708f311b81b8e86d5ab0b292c37c06bfd8ae7..cfe0063cae536946f62891795264927f9ac7ff20 100644
--- a/theories/hocap/concurrent_runners.v
+++ b/theories/hocap/concurrent_runners.v
@@ -228,7 +228,7 @@ Section contents.
     iMod (inv_alloc (N.@"task") _ (task_inv γ γ' status res (Q a))%I with "[-HP HΦ Htask Hinit]") as "#Hinv".
     { iNext. iLeft. iFrame. }
     wp_pures. iModIntro. iApply "HΦ".
-    unfold isTask, task. iFrame "#∗". eauto.
+    iFrame "#∗". eauto.
   Qed.
 
   Lemma task_Join_spec γb γ γ' (r t a : val) P Q :