diff --git a/theories/typing/own.v b/theories/typing/own.v
index 4c5e65a2f64cbe8576a98d858b0da8d1c787660e..fe897cbf96e741cf44c583c62ec34e813a9f32b5 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -234,7 +234,7 @@ Section typing.
     iIntros ([[|l|]|] tid F qmax qL ?) "_ _ $ $ Hown"; try done.
     iDestruct "Hown" as "[H↦ $]". iDestruct "H↦" as (vl) "[>H↦ #Hown]".
     iExists l, _, _. iSplitR; first done. 
-    iFrame "∗#"; auto.
+    iFrame "∗#". by iIntros "!> $".
   Qed.
 
   Lemma read_own_move E L ty n :