diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index efa91425234b0ccb55893def3264febf2fff2e8a..9f7e2faf773f4f0778ab3ce3e271783e0a195281 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-05-03.3.85295b18") | (= "dev") }
+  "coq-iris" { (= "dev.2023-06-02.4.80f55f7c") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/lang/heap.v b/theories/lang/heap.v
index ef1051a51e222db4a23fc07716d88d1f54db77e8..c147dede368126ff229137b1504fa312dc1a23a8 100644
--- a/theories/lang/heap.v
+++ b/theories/lang/heap.v
@@ -124,10 +124,11 @@ Section heap.
     AsFractional (l ↦{q} v) (λ q, l ↦{q} v)%I q.
   Proof. split; first done. apply _. Qed.
 
-  Global Instance frame_mapsto p l v q1 q2 RES :
-    FrameFractionalHyps p (l ↦{q1} v) (λ q, l ↦{q} v)%I RES q1 q2 →
-    Frame p (l ↦{q1} v) (l ↦{q2} v) RES | 5.
-  Proof. apply: frame_fractional. Qed.
+  Global Instance frame_mapsto p l v q1 q2 q :
+    FrameFractionalQp q1 q2 q →
+    Frame p (l ↦{q1} v) (l ↦{q2} v) (l ↦{q} v) | 5.
+  (* FIXME: somehow Φ gets inferred wrong here. *)
+  Proof. apply: (frame_fractional _ _ _ (λ q, l ↦{q} v)%I). Qed.
 
   Global Instance heap_mapsto_vec_timeless l q vl : Timeless (l ↦∗{q} vl).
   Proof. rewrite /heap_mapsto_vec. apply _. Qed.
diff --git a/theories/lifetime/frac_borrow.v b/theories/lifetime/frac_borrow.v
index 6d1d6468644d6fe66f9830108cad0f296a8f1aa9..d1da97f060e4710ef2d4fd3cd5d22d78510a7b4f 100644
--- a/theories/lifetime/frac_borrow.v
+++ b/theories/lifetime/frac_borrow.v
@@ -160,6 +160,9 @@ Lemma frac_bor_lft_incl `{!invGS Σ, !lftGS Σ userE, !frac_borG Σ} κ κ' q:
 Proof.
   iIntros "#LFT#Hbor". iApply lft_incl_intro. iModIntro. iSplitR.
   - iIntros (q') "Hκ'".
+    (* FIXME we should probably have a lemma for this in Iris *)
+    assert (Fractional (λ q' : Qp, (q * q').[κ']))%I.
+    { intros ??. rewrite Qp.mul_add_distr_l lft_tok_fractional //. }
     iMod (frac_bor_acc with "LFT Hbor Hκ'") as (q'') "[>? Hclose]"; first done.
     iExists _. iFrame. iIntros "!>Hκ'". iApply "Hclose". auto.
   - iIntros "H†'".
diff --git a/theories/lifetime/lifetime_sig.v b/theories/lifetime/lifetime_sig.v
index 1401bdcb0cc31fa068d4bb6de5102b5773862332..e3c8645fd1d5836ccb1c7c161a10ce45973e7fff 100644
--- a/theories/lifetime/lifetime_sig.v
+++ b/theories/lifetime/lifetime_sig.v
@@ -89,16 +89,16 @@ Module Type lifetime_sig.
   Global Declare Instance lft_tok_fractional κ : Fractional (λ q, q.[κ])%I.
   Global Declare Instance lft_tok_as_fractional κ q :
     AsFractional q.[κ] (λ q, q.[κ])%I q.
-  Global Declare Instance frame_lft_tok p κ q1 q2 RES :
-    FrameFractionalHyps p q1.[κ] (λ q, q.[κ])%I RES q1 q2 →
-    Frame p q1.[κ] q2.[κ] RES | 5.
+  Global Declare Instance frame_lft_tok p κ q1 q2 q :
+    FrameFractionalQp q1 q2 q →
+    Frame p q1.[κ] q2.[κ] q.[κ] | 5.
 
   Global Declare Instance idx_bor_own_fractional i : Fractional (λ q, idx_bor_own q i)%I.
   Global Declare Instance idx_bor_own_as_fractional i q :
     AsFractional (idx_bor_own q i) (λ q, idx_bor_own q i)%I q.
-  Global Declare Instance frame_idx_bor_own p i q1 q2 RES :
-    FrameFractionalHyps p (idx_bor_own q1 i) (λ q, idx_bor_own q i)%I RES q1 q2 →
-    Frame p (idx_bor_own q1 i) (idx_bor_own q2 i) RES | 5.
+  Global Declare Instance frame_idx_bor_own p i q1 q2 q :
+    FrameFractionalQp q1 q2 q →
+    Frame p (idx_bor_own q1 i) (idx_bor_own q2 i) (idx_bor_own q i) | 5.
 
   Global Declare Instance positive_to_lft_inj : Inj eq eq positive_to_lft.
 
diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v
index 4c5d729489b2704e0802835c369c870df7a0b5c6..edbf417439c7e4b4eae624f524d9b967577a86ee 100644
--- a/theories/lifetime/model/primitive.v
+++ b/theories/lifetime/model/primitive.v
@@ -321,10 +321,11 @@ Qed.
 Global Instance lft_tok_as_fractional κ q :
   AsFractional q.[κ] (λ q, q.[κ])%I q.
 Proof. split; first done. apply _. Qed.
-Global Instance frame_lft_tok p κ q1 q2 RES :
-  FrameFractionalHyps p q1.[κ] (λ q, q.[κ])%I RES q1 q2 →
-  Frame p q1.[κ] q2.[κ] RES | 5.
-Proof. apply: frame_fractional. Qed.
+Global Instance frame_lft_tok p κ q1 q2 q :
+    FrameFractionalQp q1 q2 q →
+    Frame p q1.[κ] q2.[κ] q.[κ] | 5.
+(* FIXME: somehow Φ gets inferred wrong here. *)
+Proof. apply: (frame_fractional _ _ _ (λ q, q.[κ])%I). Qed.
 
 Global Instance idx_bor_own_fractional i : Fractional (λ q, idx_bor_own q i)%I.
 Proof.
@@ -334,10 +335,11 @@ Qed.
 Global Instance idx_bor_own_as_fractional i q :
   AsFractional (idx_bor_own q i) (λ q, idx_bor_own q i)%I q.
 Proof. split; first done. apply _. Qed.
-Global Instance frame_idx_bor_own p i q1 q2 RES :
-  FrameFractionalHyps p (idx_bor_own q1 i) (λ q, idx_bor_own q i)%I RES q1 q2 →
-  Frame p (idx_bor_own q1 i) (idx_bor_own q2 i) RES | 5.
-Proof. apply: frame_fractional. Qed.
+Global Instance frame_idx_bor_own p i q1 q2 q :
+    FrameFractionalQp q1 q2 q →
+    Frame p (idx_bor_own q1 i) (idx_bor_own q2 i) (idx_bor_own q i) | 5.
+(* FIXME: somehow Φ gets inferred wrong here. *)
+Proof. apply: (frame_fractional _ _ _ (λ q, idx_bor_own q i)%I). Qed.
 
 (** Lifetime inclusion *)
 Lemma lft_incl_acc E κ κ' q :
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index 949e0bcd59458a8ee2161dc9ff15885fc73a2d61..b5baaa41078e01deeb02ddbc2979be3172748f36 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -96,9 +96,10 @@ Section lft_contexts.
   Global Instance llctx_interp_as_fractional qmax L q :
     AsFractional (llctx_interp_noend qmax L q) (llctx_interp_noend qmax L) q.
   Proof. split; first done. apply _. Qed.
-  Global Instance frame_llctx_interp p qmax L q1 q2 RES :
-    FrameFractionalHyps p (llctx_interp_noend qmax L q1) (llctx_interp_noend qmax L) RES q1 q2 →
-    Frame p (llctx_interp_noend qmax L q1) (llctx_interp_noend qmax L q2) RES | 5.
+  Global Instance frame_llctx_interp p qmax L q1 q2 q :
+    FrameFractionalQp q1 q2 q →
+    Frame p (llctx_interp_noend qmax L q1) (llctx_interp_noend qmax L q2)
+      (llctx_interp_noend qmax L q) | 5.
   Proof. apply: frame_fractional. Qed.
 
   Global Instance llctx_interp_permut qmax :