diff --git a/iris/program_logic/language.v b/iris/program_logic/language.v
index 98f3e685f8acc95ea4e1451bbb92d964bc77b379..280a6d36b5d44f1f87444a040d7bbf1799fed112 100644
--- a/iris/program_logic/language.v
+++ b/iris/program_logic/language.v
@@ -328,4 +328,6 @@ Section language.
 
 End language.
 
+Global Arguments step_atomic {Λ ρ1 κ ρ2}.
+
 Notation pure_steps_tp := (Forall2 (rtc pure_step)).
diff --git a/iris/program_logic/total_adequacy.v b/iris/program_logic/total_adequacy.v
index 1e95546808a97793757eaef272dbe93bc9cba3a8..a717aa5700454100ffc787dd68558dad946e2062 100644
--- a/iris/program_logic/total_adequacy.v
+++ b/iris/program_logic/total_adequacy.v
@@ -67,7 +67,7 @@ Proof.
   apply app_eq_inv in Ht as [(t&?&?)|(t&?&?)]; subst.
   - destruct t as [|e1' ?]; simplify_eq/=.
     + iMod ("IH2" with "[%] Hσ1") as (n2) "($ & Hσ & IH2 & _)".
-      { by eapply (step_atomic _ _ _ _ _ _ _ _ []). }
+      { by eapply (step_atomic _ _ _ _ _ []). }
       iModIntro. iExists n2. iFrame "Hσ".
       rewrite -{2}(left_id_L [] (++) (e2 :: _)). iApply "IH2".
       by setoid_rewrite (right_id_L [] (++)).