diff --git a/theories/typing/type.v b/theories/typing/type.v
index 0a67e7f25bcad257ddc4ab3ae143409cc086ba64..61c8cf75822784ba847840cf5d3fcd6f67ce42e0 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -121,8 +121,6 @@ Record simple_type `{!typeG Σ} :=
 Existing Instance st_own_persistent.
 Instance: Params (@st_own) 2 := {}.
 
-Arguments st_own {_ _} _ / : simpl nomatch.
-
 Program Definition ty_of_st `{!typeG Σ} (st : simple_type) : type :=
   {| ty_size := 1; ty_own := st.(st_own);
      (* [st.(st_own) tid vl] needs to be outside of the fractured