diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index ea8e14e80223c108f2943159b4b29ed0cef40dc4..e62117350312362182c55979b154454c059c1b35 100644
--- a/coq-lambda-rust.opam
+++ b/coq-lambda-rust.opam
@@ -13,7 +13,7 @@ the type system, and safety proof for some Rust libraries.
 """
 
 depends: [
-  "coq-iris" { (= "dev.2023-06-14.0.f0e415b6") | (= "dev") }
+  "coq-iris" { (= "dev.2023-08-09.1.92e6f4d4") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/lifetime/model/accessors.v b/theories/lifetime/model/accessors.v
index 971969f6dd10f58999a4bc8b2c187fd1a43f892a..945816ce2d4a65d06c6eabf5d9aaa3683faec8d2 100644
--- a/theories/lifetime/model/accessors.v
+++ b/theories/lifetime/model/accessors.v
@@ -212,7 +212,7 @@ Proof.
         iLeft. iFrame "%". iExists _, _. iFrame. }
       iMod ("Hclose" with "Htok") as "$". iExists κ''. iModIntro.
       iSplit; first by iApply lft_incl_refl. iExists j. iFrame.
-      iExists Q. rewrite -bi.iff_refl. eauto.
+      iExists Q. rewrite -(bi.iff_refl emp). auto.
     + iDestruct "Hinv" as (?) "[Hinv _]". iDestruct "Hinv" as (B ?) "[>Hinv _]".
       iDestruct (own_bor_valid_2 with "Hinv Hbor")
         as %[(_ & <- & INCL%option_included)%singleton_included_l _]%auth_both_valid_discrete.
@@ -262,7 +262,7 @@ Proof.
     rewrite own_bor_op. iDestruct "Hown" as "[H● H◯]".
     iMod ("Hclose'" with "[- Hâ—¯]"); last first.
     { iModIntro. iExists (i.1). iSplit; first by iApply lft_incl_refl.
-      iExists j. iFrame. iExists Q. rewrite -bi.iff_refl. auto. }
+      iExists j. iFrame. iExists Q. rewrite -(bi.iff_refl emp). auto. }
     iExists _, _. iFrame. rewrite big_sepS_later. iApply "Hclose''".
     iLeft. iFrame "%". iExists _, _. iFrame. iNext.
     rewrite -!fmap_delete -fmap_insert -(fmap_insert _ _ _ Bor_in).
diff --git a/theories/lifetime/model/borrow.v b/theories/lifetime/model/borrow.v
index 56adf9af2a6ed67e07d693dd94648c1a91b7974a..310bcc8396b8da1b4f567115fe2a67884d8381f8 100644
--- a/theories/lifetime/model/borrow.v
+++ b/theories/lifetime/model/borrow.v
@@ -43,7 +43,7 @@ Proof.
     iMod ("Hclose" with "[HA HI Hclose']") as "_"; [by iNext; iExists _, _; iFrame|].
     iSplitL "HBâ—¯ HsliceB".
     + rewrite /bor /raw_bor /idx_bor_own. iModIntro. iExists γB. iFrame.
-      iExists P. rewrite -bi.iff_refl. auto.
+      iExists P. rewrite -(bi.iff_refl emp). auto.
     + clear -HE. iIntros "!> H†".
       iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
       iDestruct ("HIlookup" with "HI") as %Hκ.
diff --git a/theories/lifetime/model/borrow_sep.v b/theories/lifetime/model/borrow_sep.v
index 816b02fd9bc67b1fb30aa7ac5c2bc79cb12d1b16..4541525e5ffd095614ed952f1adbe7ab9b9de723 100644
--- a/theories/lifetime/model/borrow_sep.v
+++ b/theories/lifetime/model/borrow_sep.v
@@ -51,10 +51,10 @@ Proof.
     rewrite !own_bor_op. iDestruct "Hbor" as "[[H● H◯2] H◯1]".
     iAssert (&{κ}P)%I with "[H◯1 Hs1]" as "$".
     { rewrite /bor /raw_bor /idx_bor_own. iExists κ'. iFrame "#". iExists γ1.
-      iFrame. iExists P. rewrite -bi.iff_refl. auto. }
+      iFrame. iExists P. rewrite -(bi.iff_refl emp). auto. }
     iAssert (&{κ}Q)%I with "[H◯2 Hs2]" as "$".
     { rewrite /bor /raw_bor /idx_bor_own. iExists κ'. iFrame "#". iExists γ2.
-      iFrame. iExists Q. rewrite -bi.iff_refl. auto. }
+      iFrame. iExists Q. rewrite -(bi.iff_refl emp). auto. }
     iApply "Hclose". iExists A, I. iFrame. rewrite big_sepS_later.
     iApply "Hclose'". iLeft. iFrame "%". iExists Pb', Pi. iFrame. iExists _.
     rewrite /to_borUR -!fmap_delete -!fmap_insert. iFrame "Hbox H●".
diff --git a/theories/lifetime/model/faking.v b/theories/lifetime/model/faking.v
index f899d8c2925971d2a69c01e0d5e50ee9543a7382..f0ed43dbd7dda566cf63c7077fe3bb085af0ce63 100644
--- a/theories/lifetime/model/faking.v
+++ b/theories/lifetime/model/faking.v
@@ -90,7 +90,7 @@ Proof.
     by do 2 eapply lookup_gset_to_gmap_None. }
   rewrite /bor /raw_bor /idx_bor_own /=. iModIntro. iSplitR "Hâ—¯".
   - iExists ({[γ]} ∪ B), (P ∗ Pinh)%I. rewrite !gset_to_gmap_union_singleton. by iFrame.
-  - iExists γ. iFrame. iExists P. rewrite -bi.iff_refl. eauto.
+  - iExists γ. iFrame. iExists P. rewrite -(bi.iff_refl emp). auto.
 Qed.
 
 Lemma raw_bor_fake' E κ P :
diff --git a/theories/lifetime/model/reborrow.v b/theories/lifetime/model/reborrow.v
index e6cebcceb9650a896274a4721733c407f53faaf0..bb307c2dc3c8e92f55a44703bb5adf4377a5e030 100644
--- a/theories/lifetime/model/reborrow.v
+++ b/theories/lifetime/model/reborrow.v
@@ -60,7 +60,7 @@ Proof.
      (alloc_singleton_local_update _ j (1%Qp, to_agree Bor_in)); last done.
     rewrite /to_borUR lookup_fmap. by rewrite HBj. }
   iModIntro. iExists (P ∗ Pb)%I. rewrite /Iinv. iFrame "HI Hκ". iSplitL "Hj".
-  { iExists j. iFrame. iExists P. rewrite -bi.iff_refl. auto. }
+  { iExists j. iFrame. iExists P. rewrite -(bi.iff_refl emp). auto. }
   iSplitL "Hbox HB● HB".
   { rewrite /lft_bor_alive. iNext. iExists (<[j:=Bor_in]> B).
     rewrite /to_borUR !fmap_insert big_sepM_insert //. iFrame.