diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index dc8d1118f91f2cfea5bb58cd18a01cda1aac50ff..915d6d3b183a4c122745ac0485ea7f3dcf2d4a6a 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.2022-05-13.2.6902a72f") | (= "dev") }
+  "coq-gpfsl" { (= "dev.2022-05-15.0.67fb1a52") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/lifetime/model/creation.v b/theories/lifetime/model/creation.v
index 3c375ab232e242216ba3cf91ffb03343e50d85a5..52ac3b87e6755e62636413f47ee0be98b9f405e3 100644
--- a/theories/lifetime/model/creation.v
+++ b/theories/lifetime/model/creation.v
@@ -161,7 +161,7 @@ Lemma lft_create_strong P E :
 Proof.
   assert (userE_lftN_disj:=userE_lftN_disj). iIntros (HP ?) "#LFT".
   iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
-  rewrite ->pred_infinite_set in HP.
+  rewrite ->(pred_infinite_set (C:=gset _)) in HP.
   destruct (HP (dom A)) as [Λ [HPx HΛ%not_elem_of_dom]].
   iMod (own_update with "HA") as "[HA HΛ]".
   { apply auth_update_alloc, (alloc_singleton_local_update _ Λ