diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index c341ec8696a36850e05f025a929c24a4bc92ee9e..35fef32b3d1ad802e9e42564876fd4a451163e50 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.2021-03-15.2.730f24ec") | (= "dev") }
+  "coq-iris" { (= "dev.2021-04-20.0.7a260d80") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/lifetime/model/creation.v b/theories/lifetime/model/creation.v
index a9ee1e62d335f6c0e1a6bc7cbdae44cba721ffff..5000f19bc4f4114ffa63a4bd73d6cfcc728bf975 100644
--- a/theories/lifetime/model/creation.v
+++ b/theories/lifetime/model/creation.v
@@ -175,7 +175,8 @@ Proof.
     split; last done. by eapply gmultiset_elem_of_subseteq. }
   { intros κ ???. rewrite elem_of_difference elem_of_filter elem_of_dom. auto. }
   iModIntro. iMod ("Hclose" with "[-]") as "_"; last first.
-  { iModIntro. rewrite /lft_dead. iExists Λ. rewrite elem_of_singleton. auto. }
+  { iModIntro. rewrite /lft_dead. iExists Λ.
+    rewrite gmultiset_elem_of_singleton. auto. }
   iNext. iExists (<[Λ:=false]>A), I.
   rewrite /own_alft_auth /to_alftUR fmap_insert. iFrame "HA HI".
   rewrite HI !big_sepS_union //.
diff --git a/theories/lifetime/model/definitions.v b/theories/lifetime/model/definitions.v
index 022461a936ad83a9424386266f47eefbd95636b7..f1e0adff9adf3d72a942556c034e45f06b08de58 100644
--- a/theories/lifetime/model/definitions.v
+++ b/theories/lifetime/model/definitions.v
@@ -19,7 +19,7 @@ End lft_notation.
 Definition static : lft := (∅ : gmultiset _).
 Instance lft_intersect : Meet lft := λ κ κ', κ ⊎ κ'.
 
-Definition positive_to_lft (p : positive) : lft := {[ p ]}.
+Definition positive_to_lft (p : positive) : lft := {[+ p +]}.
 
 Inductive bor_state :=
   | Bor_in
@@ -341,7 +341,7 @@ Proof. rewrite /lft_ctx. apply _. Qed.
 Global Instance positive_to_lft_inj : Inj eq eq positive_to_lft.
 Proof.
   unfold positive_to_lft. intros x y Hxy.
-  apply (elem_of_singleton_1 (C := lft)). rewrite -Hxy.
+  apply gmultiset_elem_of_singleton. rewrite -Hxy.
   set_solver.
 Qed.
 End basic_properties.