diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index 7763ae0a3a497e654374077bdec282ca06169e94..45c97d81dc1d5225c3b1d2fbd439717348df2d33 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.2024-08-16.1.b6462587") | (= "dev") }
+  "coq-gpfsl" { (= "dev.2024-08-30.0.b2983a1e") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/lifetime/model/creation.v b/theories/lifetime/model/creation.v
index 803eb3336cc27973a4b5995fcf062115b22c43f1..d2954bba8ecdb2cab8dacbae14aac5134c4734e7 100644
--- a/theories/lifetime/model/creation.v
+++ b/theories/lifetime/model/creation.v
@@ -75,7 +75,7 @@ Proof.
   { iModIntro. rewrite /Iinv. iFrame.
     iApply (@big_sepS_impl with "[$HK]"); iModIntro.
     iIntros (κ Hκ) "[(_ & _ & %)|[$ _]]". set_solver. }
-  destruct (minimal_exists_L (⊂) Kalive)
+  destruct (minimal_exists_elem_of_L (⊂) Kalive)
     as (κ & [Hκalive HκK]%elem_of_filter & Hκmin); first done.
   iDestruct (@big_sepS_delete with "HK") as "[Hκinv HK]"; first done.
   iDestruct "Hκinv" as "[(Hκ & Hκalive & _)|[_ %]]"; last first.
@@ -114,7 +114,7 @@ Proof.
   induction (set_wf K) as [K _ IH]. iIntros "HK".
   destruct (decide (K = ∅)) as [->|].
   { iExists (λ _, inhabitant). repeat (iSplit; [by auto|]). by rewrite !big_sepS_empty. }
-  destruct (minimal_exists_L (⊂) K) as (κ & HκK & Hκmin); first done.
+  destruct (minimal_exists_elem_of_L (⊂) K) as (κ & HκK & Hκmin); first done.
   rewrite big_sepS_delete //. iDestruct "HK" as "[Hinv HK]".
   iDestruct (IH with "HK") as (Vs) "(Hhv0 & Hmono & HK)". { set_solver +HκK. }
   iDestruct "Hmono" as %Hmono.