diff --git a/theories/typing/type_context.v b/theories/typing/type_context.v
index 9d354493c72622c38f54ae235c0969e2c9f653e5..ca37fc22e2714878625208d6f4879e899bd2ecf7 100644
--- a/theories/typing/type_context.v
+++ b/theories/typing/type_context.v
@@ -83,7 +83,7 @@ Section type_context.
     by iApply (Hincl with "LFT HE HL").
   Qed.
 
-  Lemma copy_tctx_incl E L p `(!Copy ty) :
+  Lemma copy_tctx_incl E L p `{!Copy ty} :
     tctx_incl E L [TCtx_hasty p ty] [TCtx_hasty p ty; TCtx_hasty p ty].
   Proof.
     iIntros (???) "_ $ $ *". rewrite /tctx_interp !big_sepL_cons big_sepL_nil.