diff --git a/theories/typing/type.v b/theories/typing/type.v
index e40f037bf38a1bf9429947f85de282be1281436a..1245b1d6596fff91999003112fb4c5ea9bf0c2d5 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -476,7 +476,7 @@ Section type.
   Qed.
 
   Lemma shr_locsE_split_tok l n m tid :
-    na_own tid (shr_locsE l (n + m)) ⊣⊢
+    na_own tid (shr_locsE l (n + m)) ⊣⊢@{vPropI _}
       na_own tid (shr_locsE l n) ∗ na_own tid (shr_locsE (l +ₗ n) m).
   Proof.
     rewrite shr_locsE_shift na_own_union //. apply shr_locsE_disj.