update dependencies

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}%"]

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))=>//.