diff --git a/theories/program_logic/language.v b/theories/program_logic/language.v
index 60d95f5b930e754bdc3ad55ebf57aef3eadb7276..d8d4b39cf033805ecbbb3c20a7f6beee0cdba12d 100644
--- a/theories/program_logic/language.v
+++ b/theories/program_logic/language.v
@@ -163,9 +163,7 @@ Section language.
 
   Lemma stuck_fill `{!@LanguageCtx Λ K} e σ :
     stuck e σ → stuck (K e) σ.
-  Proof.
-    intros ST. split; [by apply fill_not_val, ST|apply irreducible_fill; apply ST].
-  Qed.
+  Proof. intros [??]. split. by apply fill_not_val. by apply irreducible_fill. Qed.
 
   Lemma step_Permutation (t1 t1' t2 : list (expr Λ)) κ σ1 σ2 :
     t1 ≡ₚ t1' → step (t1,σ1) κ (t2,σ2) → ∃ t2', t2 ≡ₚ t2' ∧ step (t1',σ1) κ (t2',σ2).