diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index 6512c098d05fd3b0fe46b131965ec1c2e29e87f8..6f3c54526cd217e1635850c4cfa0ff24bd4b665e 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.2022-05-13.4.ab92f91e") | (= "dev") }
+  "coq-iris" { (= "dev.2022-05-13.5.de41b20f") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/lifetime/model/creation.v b/theories/lifetime/model/creation.v
index ae4457d884adfe350dbdc12d7805dd547b1d4275..6db93a1a289ceee8bfcab06c887768b7159b55f7 100644
--- a/theories/lifetime/model/creation.v
+++ b/theories/lifetime/model/creation.v
@@ -115,7 +115,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 _ Λ (Cinl 1%Qp))=>//.