diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index b4706cca993506fcb9279683a49836a1cd65635d..c5cdca0a9b42530abefa1d1b8e8379f9f7a48796 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-04-11.0.a4f8cf17") | (= "dev") }
+  "coq-iris" { (= "dev.2022-05-13.0.a1971471") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/lang/lang.v b/theories/lang/lang.v
index ab1bb8adfb35c3757da19263b07814a6485e70d8..73dd1d80ce8a44b6368e0a44f6edca837816c037 100644
--- a/theories/lang/lang.v
+++ b/theories/lang/lang.v
@@ -432,7 +432,7 @@ Proof.
 Qed.
 
 Definition fresh_block (σ : state) : block :=
-  let loclst : list loc := elements (dom _ σ : gset loc) in
+  let loclst : list loc := elements (dom σ : gset loc) in
   let blockset : gset block := foldr (λ l, ({[l.1]} ∪.)) ∅ loclst in
   fresh blockset.
 
diff --git a/theories/lifetime/model/creation.v b/theories/lifetime/model/creation.v
index 8362e9afe1e99b8e70ccb06d8b25a91ad749f553..ae4457d884adfe350dbdc12d7805dd547b1d4275 100644
--- a/theories/lifetime/model/creation.v
+++ b/theories/lifetime/model/creation.v
@@ -36,7 +36,7 @@ Proof.
   iMod (box_empty with "Hbox") as "[HP Hbox]"=>//; first by solve_ndisj.
   { intros i s. by rewrite lookup_fmap fmap_Some=> -[? [/HB -> ->]]. }
   rewrite lft_vs_unfold; iDestruct "Hvs" as (n) "[Hcnt Hvs]".
-  iDestruct (big_sepS_filter_acc (.⊂ κ) _ _ (dom _ I) with "Halive")
+  iDestruct (big_sepS_filter_acc (.⊂ κ) _ _ (dom I) with "Halive")
     as "[Halive Halive']".
   { intros κ'. rewrite elem_of_dom. eauto. }
   iApply fupd_trans. iApply fupd_mask_mono; last
@@ -50,7 +50,7 @@ Proof.
   rewrite /Iinv. iFrame "Hdead Halive' HI".
   iModIntro. iMod (lft_inh_kill with "[$Hinh $HQ]"); first set_solver+.
   iModIntro. rewrite /lft_inv_dead. iExists Q. iFrame.
-  rewrite /lft_bor_dead. iExists (dom _ B), P.
+  rewrite /lft_bor_dead. iExists (dom B), P.
   rewrite !gset_to_gmap_dom -map_fmap_compose.
   rewrite (map_fmap_ext _ ((1%Qp,.) ∘ to_agree) B); last naive_solver.
   iFrame.
@@ -102,7 +102,7 @@ Proof.
 Qed.
 
 Definition kill_set (I : gmap lft lft_names) (Λ : atomic_lft) : gset lft :=
-  filter (Λ ∈.) (dom (gset lft) I).
+  filter (Λ ∈.) (dom I).
 
 Lemma elem_of_kill_set I Λ κ : κ ∈ kill_set I Λ ↔ Λ ∈ κ ∧ is_Some (I !! κ).
 Proof. by rewrite /kill_set elem_of_filter elem_of_dom. Qed.
@@ -116,7 +116,7 @@ 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.
-  destruct (HP (dom (gset _) A)) as [Λ [HPx HΛ%not_elem_of_dom]].
+  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))=>//.
     by rewrite lookup_fmap HΛ. }
@@ -140,8 +140,8 @@ Proof.
       (exclusive_local_update _ (Cinr ())). }
   iDestruct "HΛ" as "#HΛ". iModIntro; iNext.
   pose (K := kill_set I Λ).
-  pose (K' := filter (lft_alive_in A) (dom (gset lft) I) ∖ K).
-  destruct (proj1 (subseteq_disjoint_union_L (K ∪ K') (dom (gset lft) I))) as (K''&HI&HK'').
+  pose (K' := filter (lft_alive_in A) (dom I) ∖ K).
+  destruct (proj1 (subseteq_disjoint_union_L (K ∪ K') (dom I))) as (K''&HI&HK'').
   { set_solver+. }
   assert (K ## K') by set_solver+.
   rewrite HI !big_sepS_union //. iDestruct "Hinv" as "[[HinvK HinvD] Hinv]".
diff --git a/theories/lifetime/model/definitions.v b/theories/lifetime/model/definitions.v
index a278956cfb57f526bf58010ec225ef2c184441c6..e887cdca71b1f1365807f9bbb755ed624c162ad4 100644
--- a/theories/lifetime/model/definitions.v
+++ b/theories/lifetime/model/definitions.v
@@ -135,7 +135,7 @@ Section defs.
    Definition lft_vs_inv_go (κ : lft) (lft_inv_alive : ∀ κ', κ' ⊂ κ → iProp Σ)
        (I : gmap lft lft_names) : iProp Σ :=
      (own_ilft_auth I ∗
-       [∗ set] κ' ∈ dom _ I, ∀ Hκ : κ' ⊂ κ, lft_inv_alive κ' Hκ)%I.
+       [∗ set] κ' ∈ dom I, ∀ Hκ : κ' ⊂ κ, lft_inv_alive κ' Hκ)%I.
 
    Definition lft_vs_go (κ : lft) (lft_inv_alive : ∀ κ', κ' ⊂ κ → iProp Σ)
        (Pb Pi : iProp Σ) : iProp Σ :=
@@ -179,7 +179,7 @@ Section defs.
     (∃ (A : gmap atomic_lft bool) (I : gmap lft lft_names),
       own_alft_auth A ∗
       own_ilft_auth I ∗
-      [∗ set] κ ∈ dom _ I, lft_inv A κ)%I.
+      [∗ set] κ ∈ dom I, lft_inv A κ)%I.
 
   Definition lft_ctx : iProp Σ := inv mgmtN lfts_inv.
 
@@ -263,7 +263,7 @@ Qed.
 Lemma lft_vs_inv_unfold κ (I : gmap lft lft_names) :
   lft_vs_inv κ I ⊣⊢
     own_ilft_auth I ∗
-    [∗ set] κ' ∈ dom _ I, ⌜κ' ⊂ κ⌝ → lft_inv_alive κ'.
+    [∗ set] κ' ∈ dom I, ⌜κ' ⊂ κ⌝ → lft_inv_alive κ'.
 Proof.
   rewrite /lft_vs_inv /lft_vs_inv_go. by setoid_rewrite pure_impl_forall.
 Qed.
diff --git a/theories/lifetime/model/faking.v b/theories/lifetime/model/faking.v
index 96c5f3c88e37894ec2fc0477c03b760fe81c35ec..f899d8c2925971d2a69c01e0d5e50ee9543a7382 100644
--- a/theories/lifetime/model/faking.v
+++ b/theories/lifetime/model/faking.v
@@ -9,9 +9,9 @@ Context `{!invGS Σ, !lftGS Σ userE}.
 Implicit Types κ : lft.
 
 Lemma ilft_create A I κ :
-  own_alft_auth A -∗ own_ilft_auth I -∗ ▷ ([∗ set] κ ∈ dom _ I, lft_inv A κ)
+  own_alft_auth A -∗ own_ilft_auth I -∗ ▷ ([∗ set] κ ∈ dom I, lft_inv A κ)
       ==∗ ∃ A' I', ⌜is_Some (I' !! κ)⌝ ∗
-    own_alft_auth A' ∗ own_ilft_auth I' ∗ ▷ ([∗ set] κ ∈ dom _ I', lft_inv A' κ).
+    own_alft_auth A' ∗ own_ilft_auth I' ∗ ▷ ([∗ set] κ ∈ dom I', lft_inv A' κ).
 Proof.
   iIntros "HA HI Hinv".
   destruct (decide (is_Some (I !! κ))) as [?|HIκ%eq_None_not_Some].
diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v
index 0779ffb68fd46a35a0658a9741776d43356bbde5..2635c19a705a83ac048d6330a79a05045b3819b2 100644
--- a/theories/lifetime/model/primitive.v
+++ b/theories/lifetime/model/primitive.v
@@ -160,13 +160,13 @@ Qed.
 Global Instance lft_alive_in_dec A κ : Decision (lft_alive_in A κ).
 Proof.
   refine (cast_if (decide (set_Forall (λ Λ, A !! Λ = Some true)
-                  (dom (gset atomic_lft) κ))));
+                  (dom κ))));
     rewrite /lft_alive_in; by setoid_rewrite <-gmultiset_elem_of_dom.
 Qed.
 Global Instance lft_dead_in_dec A κ : Decision (lft_dead_in A κ).
 Proof.
   refine (cast_if (decide (set_Exists (λ Λ, A !! Λ = Some false)
-                  (dom (gset atomic_lft) κ))));
+                  (dom κ))));
       rewrite /lft_dead_in; by setoid_rewrite <-gmultiset_elem_of_dom.
 Qed.
 
@@ -174,9 +174,9 @@ Lemma lft_alive_or_dead_in A κ :
   (∃ Λ, Λ ∈ κ ∧ A !! Λ = None) ∨ (lft_alive_in A κ ∨ lft_dead_in A κ).
 Proof.
   rewrite /lft_alive_in /lft_dead_in.
-  destruct (decide (set_Exists (λ Λ, A !! Λ = None) (dom (gset _) κ)))
+  destruct (decide (set_Exists (λ Λ, A !! Λ = None) (dom κ)))
     as [(Λ & ?%gmultiset_elem_of_dom & HAΛ)|HA%(not_set_Exists_Forall _)]; first eauto.
-  destruct (decide (set_Exists (λ Λ, A !! Λ = Some false) (dom (gset _) κ)))
+  destruct (decide (set_Exists (λ Λ, A !! Λ = Some false) (dom κ)))
     as [(Λ & HΛ%gmultiset_elem_of_dom & ?)|HA'%(not_set_Exists_Forall _)]; first eauto.
   right; left. intros Λ HΛ%gmultiset_elem_of_dom.
   move: (HA _ HΛ) (HA' _ HΛ)=> /=. case: (A !! Λ)=>[[]|]; naive_solver.
diff --git a/theories/lifetime/model/reborrow.v b/theories/lifetime/model/reborrow.v
index d43ac391e9dc94a1d1313fd69050d68fef92f2c3..e6cebcceb9650a896274a4721733c407f53faaf0 100644
--- a/theories/lifetime/model/reborrow.v
+++ b/theories/lifetime/model/reborrow.v
@@ -89,7 +89,7 @@ Proof.
   iMod ("Hvs" $! I with "[HI Hinv Hvs' Hinh HB● Hbox HB]
                          [$HPb $Hi] Hκ†") as "($ & $ & Hcnt')".
   { rewrite lft_vs_inv_unfold. iFrame "HI".
-    iApply (big_sepS_delete _ (dom (gset lft) I) with "[- $Hinv]"); first done.
+    iApply (big_sepS_delete _ (dom I) with "[- $Hinv]"); first done.
     iIntros (_). rewrite lft_inv_alive_unfold.
     iExists Pb', Pi'. iFrame "Hvs' Hinh". rewrite /lft_bor_alive.
     iExists (<[i:=Bor_in]>B'). rewrite /to_borUR !fmap_insert. iFrame.
@@ -111,7 +111,7 @@ Proof.
   { rewrite /lft_inv_dead. iDestruct "Hinvκ" as (Pi) "[Hbordead H]".
     iMod (raw_bor_fake with "Hbordead") as "[Hbordead $]"; first solve_ndisj.
     iApply "Hclose". iExists _, _. iFrame.
-    rewrite (big_opS_delete _ (dom _ _) κ') ?elem_of_dom // /lft_inv /lft_inv_dead.
+    rewrite (big_opS_delete _ (dom _) κ') ?elem_of_dom // /lft_inv /lft_inv_dead.
     auto 10 with iFrame. }
   rewrite {1}/raw_bor. iDestruct "Hraw" as (i') "[Hbor H]".
   iDestruct "H" as (P') "[#HP' #Hs']".
@@ -141,7 +141,7 @@ Proof.
     iRewrite "HeqPb'". iFrame. by iApply "HP'". }
   iDestruct "HH" as "([HI Hinvκ] & $ & Halive & Hvs)".
   iApply "Hclose". iExists _, _. iFrame.
-  rewrite (big_opS_delete _ (dom _ _) κ') ?elem_of_dom //.
+  rewrite (big_opS_delete _ (dom _) κ') ?elem_of_dom //.
   iDestruct ("Hclose'" with "Hinvκ") as "$".
   rewrite /lft_inv lft_inv_alive_unfold. auto 10 with iFrame.
 Qed.