Merge branch 'ike/fix_limit_iframe_ex' into 'master'

Fix proof after iris!1035.

See merge request !36

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 :