diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index 99df3cd082003228f9d76ac9d5978a853d5230b7..1a16b6ab325e96befb066e829b36d4e12eedeca5 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-09-30.0.941e58fb") | (= "dev") }
+  "coq-gpfsl" { (= "dev.2023-10-03.0.41e501bd") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/lifetime/model/creation.v b/theories/lifetime/model/creation.v
index 2281b1a7891c586939ea3c316ee5f55e9f486177..803eb3336cc27973a4b5995fcf062115b22c43f1 100644
--- a/theories/lifetime/model/creation.v
+++ b/theories/lifetime/model/creation.v
@@ -81,7 +81,7 @@ Proof.
   iDestruct "Hκinv" as "[(Hκ & Hκalive & _)|[_ %]]"; last first.
   { by destruct (lft_alive_and_dead_in A κ). }
   assert (κ ∉ K') as HκK' by set_solver +HκK HKK'.
-  specialize (IH (K ∖ {[ κ ]})). feed specialize IH; [set_solver +HκK|set_solver +HVs|].
+  ospecialize (IH (K ∖ {[ κ ]}) _ _); [set_solver +HκK|set_solver +HVs|].
   iMod (IH ({[ κ ]} ∪ K') with "[HI Halive Hκalive] HK") as "[[HI Halive] Hdead]".
   { set_solver +HKK'. }
   { rewrite [_ ∪ K'](comm (R:=eq)) -(assoc (R:=eq) (∪)) -union_difference_L //