diff --git a/theories/typing/unsafe/cell.v b/theories/typing/unsafe/cell.v
index 878c6ba0735a0e23a7663e0fc5602131ff1d825c..687b41cc392b5ba3da236dec71554421b55659e2 100644
--- a/theories/typing/unsafe/cell.v
+++ b/theories/typing/unsafe/cell.v
@@ -103,7 +103,7 @@ Section typing.
   Definition cell_get_mut : val :=
     funrec: <> ["x"] := "return" ["x"].
 
-  Lemma cell_get_mut_type `(!Copy ty) :
+  Lemma cell_get_mut_type ty :
     typed_instruction_ty [] [] [] cell_get_mut
       (fn (λ α, [☀α])%EL (λ α, [# &uniq{α} (cell ty)])%T (λ α, &uniq{α} ty)%T).
   Proof.