diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index 472a350afcc937a9cf67729753decd1db6399b27..228746eea6dbf4caf69bbce212efd98857efd022 100644
--- a/coq-lambda-rust.opam
+++ b/coq-lambda-rust.opam
@@ -15,7 +15,7 @@ This branch uses a proper weak memory model.
 """
 
 depends: [
-  "coq-gpfsl" { (= "dev.2023-05-07.0.9cf7aca0") | (= "dev") }
+  "coq-gpfsl" { (= "dev.2023-06-05.0.4b355a65") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/lifetime/frac_borrow.v b/theories/lifetime/frac_borrow.v
index 795a764b45e1ff31332f3ba1e8b8306e58d6704d..a0b313e2b6f4514c2aa5827a6c84e376f07de2f2 100644
--- a/theories/lifetime/frac_borrow.v
+++ b/theories/lifetime/frac_borrow.v
@@ -103,7 +103,9 @@ Section frac_bor.
     ↑lftN ⊆ E → ⎡lft_ctx⎤ -∗ &{κ}P ={E}=∗ &frac{κ}φ.
   Proof.
     iIntros (?) "#? ?". rewrite [P]as_fractional. iApply bor_fracture'=>//.
-    iIntros "!> !> %%". by rewrite fractional -(bi.iff_refl True%I).
+    iIntros "!> !> %%".
+    assert (Fractional φ). { by apply : as_fractional_fractional. }
+    by rewrite fractional -(bi.iff_refl True%I).
   Qed.
 
   Lemma frac_bor_acc `{LatBottom Lat} φ E q κ :
diff --git a/theories/lifetime/lifetime.v b/theories/lifetime/lifetime.v
index b9bd9420e02a8df520a2e93d021e59ea01e7d9ec..7a260b4e26cebc1d45802c0ed63a68424827df77 100644
--- a/theories/lifetime/lifetime.v
+++ b/theories/lifetime/lifetime.v
@@ -1,4 +1,5 @@
 From orc11 Require Export base.
+Require Import iris.bi.lib.fractional.
 From lrust.lifetime Require Export lifetime_sig.
 From lrust.lifetime.model Require definitions primitive accessors faking borrow
      borrow_sep reborrow creation in_at_borrow.
@@ -32,6 +33,10 @@ Section derived.
 Context `{!invGS Σ, !lftG Σ Lat userE}.
 Implicit Types κ : lft.
 
+(* TODO: upstream *)
+Global Instance lft_mul_fractional q κ : Fractional (λ q', (q * q').[κ])%I.
+Proof. intros ??. by rewrite Qp.mul_add_distr_l lft_tok_fractional. Qed.
+
 Lemma lft_create E `{LatBottom Lat} :
   ↑lftN ⊆ E →
    ⎡lft_ctx⎤ ={E}=∗ ∃ κ, 1.[κ] ∗ □ (1.[κ] ={↑lftN ∪ userE}[userE]▷=∗ [†κ]).
diff --git a/theories/lifetime/lifetime_sig.v b/theories/lifetime/lifetime_sig.v
index c41ee4ebd3c24d502daea7ee33af6af3c997b7ee..958cb00dc95e8e0d9e659679ba166b3db26a4f6a 100644
--- a/theories/lifetime/lifetime_sig.v
+++ b/theories/lifetime/lifetime_sig.v
@@ -110,9 +110,9 @@ 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 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 2df819b890306181967479a74fec096178c48214..e9f6bbd238bd6326668807a2a5df65dd980d9979 100644
--- a/theories/lifetime/model/primitive.v
+++ b/theories/lifetime/model/primitive.v
@@ -325,10 +325,10 @@ Qed.
 Global Instance lft_tok_as_fractional κ q :
   AsFractional (q.[κ]) (λ q, q.[κ])%I q.
 Proof. split; [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.
+Proof. apply: (frame_fractional (λ q, q.[κ])%I). Qed.
 
 Lemma lft_tok_split_obj `{LatBottom Lat bot} q1 q2 κ :
   (q1 + q2).[κ] -∗ q1.[κ] ∗ <obj> q2.[κ].
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index 7e28f6f8cb2bcc9d7bec30155ea7dfd89b9ffac3..3fcb787281d77eb3af67da863736468046bdf51b 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -96,9 +96,9 @@ 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 :
diff --git a/theories/typing/lib/brandedvec.v b/theories/typing/lib/brandedvec.v
index 4c7d6a163b68087f2570e102bd74c1cfce786d31..d2d8fc0f1e68cea6a3ca410b8c77951a01fd778e 100644
--- a/theories/typing/lib/brandedvec.v
+++ b/theories/typing/lib/brandedvec.v
@@ -46,7 +46,8 @@ Section brandedvec.
     iMod (bor_share brandvecN with "Hghost") as "Hghost"; first solve_ndisj.
     iMod (bor_persistent with "LFT Hown Hκ") as "[> % $]"; first solve_ndisj.
     subst. iExists n. iFrame.
-    by iApply (bor_fracture with "LFT"); first solve_ndisj.
+    by iApply (bor_fracture with "LFT");
+      [apply fractional.fractional_as_fractional, _|solve_ndisj|].
   Qed.
   Next Obligation.
     iIntros (ty ?? tid l) "#H⊑ H".
@@ -93,7 +94,8 @@ Section brandedvec.
     iMod (bor_persistent with "LFT Hghost Hκ") as "[>Hghost $]"; first solve_ndisj.
     iDestruct "Hghost" as (m) "[Hghost %]". subst vl.
     iExists m. iFrame.
-    by iApply (bor_fracture with "LFT"); first solve_ndisj.
+    by iApply (bor_fracture with "LFT");
+      [apply fractional.fractional_as_fractional, _|solve_ndisj|].
   Qed.
   Next Obligation.
     iIntros (ty ?? tid l) "#H⊑ H".