From f5db79bcf8b940250e30df06e48cd7e89de36476 Mon Sep 17 00:00:00 2001
From: Hoang-Hai Dang <haidang@mpi-sws.org>
Date: Fri, 13 May 2022 21:14:52 +0200
Subject: [PATCH] bump gpfsl

---
 coq-lambda-rust.opam                  |  2 +-
 theories/lifetime/model/accessors.v   | 13 ++++++++-----
 theories/lifetime/model/boxes.v       |  2 +-
 theories/lifetime/model/creation.v    | 28 +++++++++++++--------------
 theories/lifetime/model/definitions.v | 10 +++++-----
 theories/lifetime/model/faking.v      | 22 ++++++++++-----------
 theories/lifetime/model/primitive.v   | 22 ++++++++++-----------
 theories/lifetime/model/reborrow.v    |  8 ++++----
 8 files changed, 55 insertions(+), 52 deletions(-)

diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index 67d305fd..dc8d1118 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-03-21.1.cf3ee78d") | (= "dev") }
+  "coq-gpfsl" { (= "dev.2022-05-13.2.6902a72f") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/lifetime/model/accessors.v b/theories/lifetime/model/accessors.v
index 6345d17c..e7b59778 100644
--- a/theories/lifetime/model/accessors.v
+++ b/theories/lifetime/model/accessors.v
@@ -147,7 +147,7 @@ Lemma idx_bor_acc_internal E q κ s P Vbor Vtok :
 Proof.
   iIntros (HE1 HE2) "#LFT #Hs Hbor Htok".
   iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
-  iAssert ⌜κ ∈ dom (gset _) I⌝%I as %Hκ'.
+  iAssert ⌜κ ∈ dom I⌝%I as %Hκ'.
   { unfold idx_bor_own. iDestruct "Hbor" as (Vb) "[% Hbor]".
     iApply (own_bor_auth with "HI Hbor"). }
   rewrite big_sepS_later big_sepS_elem_of_acc //. rewrite [lft_inv _ κ]/lft_inv.
@@ -184,7 +184,7 @@ Proof.
   { solve_ndisj. } { done. }
   iMod (extend_lft_view with "Htok HA") as (A') "($ & HA' & %)".
   iApply "Hclose". iExists _, _. iFrame.
-  rewrite big_sepS_later (big_sepS_delete _ (dom _ I)) //. iSplitR "Hclose'".
+  rewrite big_sepS_later (big_sepS_delete _ (dom I)) //. iSplitR "Hclose'".
   - unfold lft_inv. iExists (Vtok' ⊔ Vκ). iSplit; [by eauto using ame_hv_κ|]. iLeft. iSplit.
     + rewrite lft_inv_alive_unfold. iExists _, _. iFrame.
     + eauto using ame_lft_alive_in.
@@ -194,6 +194,9 @@ Qed.
 (** Indexed borrow *)
 Lemma idx_bor_acc E q κ i P Vtok Vbor:
   ↑lftN ⊆ E →
+  (*
+  ⎡lft_ctx⎤ -∗ &{κ,i}P -∗ @{Vbor} idx_bor_own i -∗ q.[κ] ={E}=∗
+    ∃ V, ⌜V ⊑ Vbor⌝ ∗ ⊔{V} ▷ P ∗ (⊔{V} ▷ P ={E}=∗ ⊔{V} idx_bor_own i ∗ q.[κ]). *)
   lft_ctx -∗ &{κ,i}P Vtok -∗ idx_bor_own i Vbor -∗ q.[κ] Vtok ={E}=∗
     ∃ V, ⌜V ⊑ Vbor ⊔ Vtok⌝ ∗ ▷ P V ∗
           (∀ Vtok', ⌜Vtok ⊑ Vtok'⌝ -∗ ▷ P (Vtok' ⊔ V)
@@ -245,7 +248,7 @@ Proof.
   iDestruct "Hs" as (P') "[#HPP' Hs]".
   iMod (lft_incl_acc with "Hle Htok") as (q') "[Htok Hclose]". { solve_ndisj. }
   iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose'".
-  iAssert (⌜κ'' ∈ dom (gset _) I⌝)%I as %Hκ'.
+  iAssert (⌜κ'' ∈ dom I⌝)%I as %Hκ'.
   { unfold idx_bor_own. iDestruct "Hbor" as (Vb) "[#HVb Hbor]".
     rewrite -embed_pure. iApply (own_bor_auth with "HI Hbor"). }
   rewrite big_sepS_later big_sepS_elem_of_acc //. rewrite [lft_inv _ κ'']/lft_inv.
@@ -309,7 +312,7 @@ Proof.
   iMod (extend_lft_view with "Htok HA") as (A') "(Htok & HA' & %)".
   iMod ("Hclose'" with "[-Hbor Htok Hclose]") as "_".
   { iModIntro. iModIntro. iExists _, _. iFrame.
-    rewrite (big_sepS_delete _ (dom _ I)) //. iSplitR "Hclose''".
+    rewrite (big_sepS_delete _ (dom I)) //. iSplitR "Hclose''".
     - unfold lft_inv. iExists (V' ⊔ Vκ). iSplit; [by eauto using ame_hv_κ|]. iLeft. iSplit.
       + rewrite lft_inv_alive_unfold /lft_bor_alive. iExists _, _.
         iFrame "Hinh". iSplitL "Halive"; [iDestruct "Halive" as (?) "?"; by iExists _|].
@@ -339,7 +342,7 @@ Proof.
   iDestruct "Hbor" as (i) "((#Hle & #Hs) & Hbor)".
   iDestruct "Hs" as (P') "[#HPP' Hs]".
   iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose'".
-  iAssert (⌜i.1 ∈ dom (gset _) I⌝)%I as %Hκ'.
+  iAssert (⌜i.1 ∈ dom I⌝)%I as %Hκ'.
   { unfold idx_bor_own. iDestruct "Hbor" as (Vb) "[#HVb Hbor]".
     by iDestruct (own_bor_auth with "HI Hbor") as "%". }
   rewrite big_sepS_later big_sepS_elem_of_acc //. rewrite [lft_inv _ (i.1)]/lft_inv.
diff --git a/theories/lifetime/model/boxes.v b/theories/lifetime/model/boxes.v
index 4fc6222b..fdc0827a 100644
--- a/theories/lifetime/model/boxes.v
+++ b/theories/lifetime/model/boxes.v
@@ -127,7 +127,7 @@ Lemma slice_insert_empty E q f Q P :
 Proof.
   iDestruct 1 as (Φ) "[#HeqP Hf]".
   iMod (own_alloc_cofinite (●E None ⋅ ◯E None,
-    Some (to_agree (Next (Q : _ -d> _)))) (dom _ f))
+    Some (to_agree (Next (Q : _ -d> _)))) (dom f))
     as (γ) "[Hdom Hγ]". { split; [by apply excl_auth_valid|done]. }
   rewrite pair_split. iDestruct "Hγ" as "[[Hγ Hγ'] #HγQ]".
   iDestruct "Hdom" as % ?%not_elem_of_dom.
diff --git a/theories/lifetime/model/creation.v b/theories/lifetime/model/creation.v
index 1cc711b4..3c375ab2 100644
--- a/theories/lifetime/model/creation.v
+++ b/theories/lifetime/model/creation.v
@@ -11,13 +11,13 @@ Implicit Types κ : lft.
 Local Set Default Proof Using "Type*".
 
 Lemma lft_kill (I : gmap lft lft_names) (K K' : gset lft) (κ : lft) (Vs : lft → Lat) :
-  (∀ κ', κ' ∈ dom (gset _) I → κ' ⊆ κ → Vs κ ⊑ Vs κ') →
+  (∀ κ', κ' ∈ dom I → κ' ⊆ κ → Vs κ ⊑ Vs κ') →
   let Iinv := (
     own_ilft_auth I ∗
     ([∗ set] κ' ∈ K, lft_inv_dead κ' (Vs κ')) ∗
     ([∗ set] κ' ∈ K', lft_inv_alive κ' (Vs κ')))%I in
-  (∀ κ', κ' ∈ dom (gset _) I → κ ⊂ κ' → κ' ∈ K) →
-  (∀ κ', κ' ∈ dom (gset _) I → κ' ⊂ κ → κ' ∈ K') →
+  (∀ κ', κ' ∈ dom I → κ ⊂ κ' → κ' ∈ K) →
+  (∀ κ', κ' ∈ dom I → κ' ⊂ κ → κ' ∈ K') →
   Iinv -∗ lft_inv_alive κ (Vs κ) -∗ (∃ V, [†κ] V)
   ={userE ∪ ↑borN ∪ ↑inhN}=∗ Iinv ∗ lft_inv_dead κ (Vs κ).
 Proof.
@@ -39,7 +39,7 @@ Proof.
   iMod (box_empty with "Hbox") as "[HP Hbox]"=>//; first set_solver+.
   { intros i s. by rewrite lookup_fmap fmap_Some=>-[? [/HB [?[-> ?]] ->]] /=. }
   rewrite lft_vs_unfold; iDestruct "Hvs" as (Vκ n) "(% & Hcnt & Hvs)".
-  iDestruct (big_sepS_filter_acc (.⊂ κ) _ _ (dom _ I) with "Halive")
+  iDestruct (big_sepS_filter_acc (.⊂ κ) _ _ (dom I) with "Halive")
     as "[Halive Halive']"; [by eauto|].
   iApply fupd_trans. iApply (fupd_mask_mono (userE ∪ ↑borN)); [set_solver+|].
   iMod ("Hvs" $! I Vs with "[//] [//] [HI Halive] HP Hκ") as "(Hinv & HQ & Hcnt')".
@@ -59,9 +59,9 @@ Qed.
 
 Lemma lfts_kill A (I : gmap lft lft_names) (K K' : gset lft) (Vs : lft → Lat) :
   let Iinv K' := (own_ilft_auth I ∗ [∗ set] κ' ∈ K', lft_inv_alive κ' (Vs κ'))%I in
-  (∀ κ κ', κ ∈ K → κ' ∈ dom (gset _) I → κ' ⊆ κ → Vs κ ⊑ Vs κ') →
-  K ## K' → dom (gset _) I = K' ∪ K  →
-  (∀ κ κ', κ ∈ K → κ' ∈ dom (gset _) I → κ ⊆ κ' → κ' ∈ K) →
+  (∀ κ κ', κ ∈ K → κ' ∈ dom I → κ' ⊆ κ → Vs κ ⊑ Vs κ') →
+  K ## K' → dom I = K' ∪ K  →
+  (∀ κ κ', κ ∈ K → κ' ∈ dom I → κ ⊆ κ' → κ' ∈ K) →
   Iinv K' -∗ ([∗ set] κ ∈ K,
      (∃ V, [†κ] V) ∗ lft_inv_alive κ (Vs κ) ∗ ⌜@lft_alive_in Lat A κ⌝ ∨
      lft_inv_dead κ (Vs κ) ∗ ⌜lft_dead_in A κ⌝)
@@ -162,7 +162,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, to_latT bot)))=>//. by rewrite lookup_fmap HΛ. }
@@ -208,14 +208,14 @@ Proof.
     by eapply auth_update, singleton_local_update,
        (exclusive_local_update _ (Cinr (to_agree (to_latT (Vs {[Λ]}))))). }
   iDestruct "HΛ" as "#HΛ". iModIntro; iNext.
-  pose (K' := filter (λ κ, lft_alive_in A κ ∧ Λ ∉ κ) (dom (gset lft) I)).
-  destruct (proj1 (subseteq_disjoint_union_L K' (dom (gset lft) I))) as (K&HI&HK).
+  pose (K' := filter (λ κ, lft_alive_in A κ ∧ Λ ∉ κ) (dom I)).
+  destruct (proj1 (subseteq_disjoint_union_L K' (dom I))) as (K&HI&HK).
   { set_solver+. }
-  assert (elem_of_K : ∀ κ, κ ∈ K ↔ κ ∈ dom (gset _) I ∧ (lft_dead_in A κ ∨ Λ ∈ κ)).
+  assert (elem_of_K : ∀ κ, κ ∈ K ↔ κ ∈ dom I ∧ (lft_dead_in A κ ∨ Λ ∈ κ)).
   { rewrite HI=>κ. rewrite elem_of_union elem_of_filter. split.
     - intros HκK. split; [by auto|]. destruct (decide (Λ ∈ κ)) as [|HΛκ]; [by auto|left].
       destruct (lft_alive_or_dead_in A κ) as [(Λ'&HΛ'&EQΛ')|[Hal|?]]=>//.
-      + exfalso. assert (κ ∈ dom (gset _) I). { by set_solver+HI HκK. }
+      + exfalso. assert (κ ∈ dom I). { by set_solver+HI HκK. }
         assert (lft_has_view A κ (Vs κ)) as Hhv' by auto.
         specialize (Hhv' Λ' HΛ'). by rewrite EQΛ' in Hhv'.
       + edestruct HK=>//. set_solver + Hal HΛκ HκK HI.
@@ -223,7 +223,7 @@ Proof.
   rewrite HI !big_sepS_union //. iDestruct "Hinv" as "[HinvD HinvK]".
   iApply fupd_trans. iApply (fupd_mask_mono (userE ∪ ↑borN ∪ ↑inhN)); first solve_ndisj.
   iMod (lfts_kill A I K K' Vs with "[$HI HinvD] [HinvK]") as "[[HI HinvD] HinvK]"=>//.
-  { intros κ κ' Hκ Hκ' Hκκ'. assert (κ ∈ dom (gset _) I) by set_solver +HI Hκ. auto. }
+  { intros κ κ' Hκ Hκ' Hκκ'. assert (κ ∈ dom I) by set_solver +HI Hκ. auto. }
   { move=> κ κ'. rewrite !elem_of_K=>-[?[Hd|?]] ??; split=>//.
     - left. destruct Hd as (Λ'&?&?). exists Λ'. split; [|done].
       by eapply gmultiset_elem_of_subseteq.
@@ -243,7 +243,7 @@ Proof.
     case: (A!!Λ)=>[[??]|]; [|intros EQ; by inversion EQ]. simpl.
     intros [_ ->]%(inj Some)%(inj2 pair)=>/(_ eq_refl) <- //. }
   set (A' := <[Λ:=(false, Vs {[+ Λ +]})]>A).
-  assert (Hhv : ∀ κ, κ ∈ dom (gset _) I → lft_has_view A' κ (Vs κ)).
+  assert (Hhv : ∀ κ, κ ∈ dom I → lft_has_view A' κ (Vs κ)).
   { intros κ Hκ Λ' HΛ'. assert (Hhv : lft_has_view A κ (Vs κ)) by auto.
     specialize (Hhv Λ' HΛ').
     destruct (decide (Λ =  Λ')) as [<-|]; rewrite ?lookup_insert ?lookup_insert_ne //=.
diff --git a/theories/lifetime/model/definitions.v b/theories/lifetime/model/definitions.v
index 067b37e0..5c68ed5d 100644
--- a/theories/lifetime/model/definitions.v
+++ b/theories/lifetime/model/definitions.v
@@ -143,7 +143,7 @@ Section defs.
    Definition lft_vs_inv_go (κ : lft) (lft_inv_alive : ∀ κ', κ' ⊂ κ → Lat → iProp)
        (Vs : lft → Lat) (I : gmap lft lft_names) : iProp :=
      (own_ilft_auth I ∗
-       [∗ set] κ' ∈ dom _ I, ∀ Hκ : κ' ⊂ κ, lft_inv_alive κ' Hκ (Vs κ'))%I.
+       [∗ set] κ' ∈ dom I, ∀ Hκ : κ' ⊂ κ, lft_inv_alive κ' Hκ (Vs κ'))%I.
 
    Definition lft_vs_go (κ : lft) (lft_inv_alive : ∀ κ', κ' ⊂ κ → monPred)
               (Pb Pi : monPred) : monPred :=
@@ -151,7 +151,7 @@ Section defs.
         ⎡own_cnt κ (● n) ∗
          ∀ (I : gmap lft lft_names) (Vs : lft → Lat),
            ⌜Vκ ⊑ Vs κ⌝ -∗
-           ⌜∀ κ', κ' ∈ dom (gset _) I → κ' ⊆ κ → Vs κ ⊑ Vs κ'⌝ -∗
+           ⌜∀ κ', κ' ∈ dom I → κ' ⊆ κ → Vs κ ⊑ Vs κ'⌝ -∗
            lft_vs_inv_go κ lft_inv_alive Vs I -∗ ▷ Pb (Vs κ) -∗ (∃ V, lft_dead κ V)
              ={userE ∪ ↑borN}=∗
            lft_vs_inv_go κ lft_inv_alive Vs I ∗ ▷ Pi (Vs κ) ∗ own_cnt κ (◯ n)⎤)%I.
@@ -190,7 +190,7 @@ Section defs.
     (∃ (A : gmap atomic_lft (bool * Lat)) (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.
 
@@ -281,7 +281,7 @@ Qed.
 Lemma lft_vs_inv_unfold κ (I : gmap lft lft_names) Vs :
   lft_vs_inv κ Vs I ⊣⊢
     own_ilft_auth I ∗
-    [∗ set] κ' ∈ dom _ I, ⌜κ' ⊂ κ⌝ → lft_inv_alive κ' (Vs κ').
+    [∗ set] κ' ∈ dom I, ⌜κ' ⊂ κ⌝ → lft_inv_alive κ' (Vs κ').
 Proof.
   rewrite /lft_vs_inv /lft_vs_inv_go. by setoid_rewrite bi.pure_impl_forall.
 Qed.
@@ -290,7 +290,7 @@ Lemma lft_vs_unfold κ Pb Pi :
     ⎡own_cnt κ (● n) ∗
      ∀ (I : gmap lft lft_names) (Vs : lft → Lat),
        ⌜Vκ ⊑ Vs κ⌝ -∗
-       ⌜∀ κ', κ' ∈ dom (gset _) I → κ' ⊆ κ → Vs κ ⊑ Vs κ'⌝ -∗
+       ⌜∀ κ', κ' ∈ dom I → κ' ⊆ κ → Vs κ ⊑ Vs κ'⌝ -∗
        lft_vs_inv κ Vs I -∗ ▷ Pb (Vs κ) -∗ (∃ V, lft_dead κ V) ={userE ∪ ↑borN}=∗
        lft_vs_inv κ Vs I ∗ ▷ Pi (Vs κ) ∗ own_cnt κ (◯ n)⎤.
 Proof. done. Qed.
diff --git a/theories/lifetime/model/faking.v b/theories/lifetime/model/faking.v
index b499f090..8f9598c8 100644
--- a/theories/lifetime/model/faking.v
+++ b/theories/lifetime/model/faking.v
@@ -11,9 +11,9 @@ Implicit Types κ : lft.
 Local Set Default Proof Using "Type*".
 
 Lemma ilft_create A I κ :
-  own_alft_auth A -∗ own_ilft_auth I -∗ ▷ ([∗ set] κ ∈ dom _ I, lft_inv A κ)
-    ==∗ ∃ A' I', ⌜κ ∈ dom (gset _) 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', ⌜κ ∈ dom I'⌝ ∗
+      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].
@@ -49,27 +49,27 @@ Proof.
         iSplitR; [iApply box_alloc|]. rewrite /own_bor. iExists γs. by iFrame. }
       iSplitR "Hinh"; last by iApply "Hinh".
       rewrite lft_vs_unfold. iExists bot, 0. iSplit=>//. iFrame "Hcnt Hcnt'". auto. }
-  set (A' := union_with (λ x _, Some x) A (gset_to_gmap (false, bot) (dom _ κ))).
+  set (A' := union_with (λ x _, Some x) A (gset_to_gmap (false, bot) (dom κ))).
   iMod (own_update _ _ (● to_alftUR A' ⋅ _) with "HA") as "[HA _]".
   { apply auth_update_alloc.
     assert (to_alftUR A'
-      ≡ gset_to_gmap (Cinr (to_agree $ to_latT bot)) (dom _ κ ∖ dom _ A) ⋅ to_alftUR A) as ->.
+      ≡ gset_to_gmap (Cinr (to_agree $ to_latT bot)) (dom κ ∖ dom A) ⋅ to_alftUR A) as ->.
     { intros Λ. rewrite lookup_op lookup_gset_to_gmap !lookup_fmap lookup_union_with
         lookup_gset_to_gmap.
       destruct (A !! Λ) eqn:EQ.
-      - apply (elem_of_dom_2 (D:=gset atomic_lft)) in EQ.
+      - apply elem_of_dom_2 in EQ.
         rewrite [X in _ ≡ X ⋅ _]option_guard_False; last set_solver. by destruct mguard.
-      - apply (not_elem_of_dom (D:=gset atomic_lft)) in EQ.
-        destruct (decide (Λ ∈ dom (gset _) κ)).
+      - apply not_elem_of_dom in EQ.
+        destruct (decide (Λ ∈ dom κ)).
         + rewrite !option_guard_True; set_solver.
         + rewrite !option_guard_False; set_solver. }
     eapply op_local_update_discrete=>HA Λ. specialize (HA Λ).
     rewrite lookup_op lookup_gset_to_gmap !lookup_fmap.
     destruct (A !! Λ) eqn:EQ.
-    - apply (elem_of_dom_2 (D:=gset atomic_lft)) in EQ.
+    - apply elem_of_dom_2 in EQ.
       rewrite option_guard_False; [by destruct p as [[]?]|set_solver].
-    - apply (not_elem_of_dom (D:=gset atomic_lft)) in EQ.
-      destruct (decide (Λ ∈ dom (gset _) κ)).
+    - apply not_elem_of_dom in EQ.
+      destruct (decide (Λ ∈ dom κ)).
       + rewrite !option_guard_True; [done|set_solver].
       + rewrite !option_guard_False; [done|set_solver]. }
   iExists A', (<[κ:=γs]> I). iFrame "HA". iModIntro.
diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v
index b1d80bdf..2c28f676 100644
--- a/theories/lifetime/model/primitive.v
+++ b/theories/lifetime/model/primitive.v
@@ -32,7 +32,7 @@ Qed.
 (** Ownership *)
 Lemma own_ilft_auth_agree (I : gmap lft lft_names) κ γs :
   own_ilft_auth I -∗
-    own ilft_name (◯ {[κ := to_agree γs]}) -∗ ⌜κ ∈ dom (gset _) I⌝.
+    own ilft_name (◯ {[κ := to_agree γs]}) -∗ ⌜κ ∈ dom I⌝.
 Proof.
   iIntros "HI Hκ". iDestruct (own_valid_2 with "HI Hκ")
     as %[[? [Hl ?]]%singleton_included_l _]%auth_both_valid_discrete.
@@ -40,7 +40,7 @@ Proof.
   destruct (fmap_Some_equiv_1 _ _ _ Hl) as (?&?&?). eauto.
 Qed.
 
-Lemma own_alft_auth_agree (A : gmap atomic_lft (bool * Lat)) Λ bV :
+Lemma own_alft_auth_agree (A : gmap atomic_lft (bool * Lat)) Λ (bV : (bool * Lat)) :
   own_alft_auth A -∗
     own alft_name (◯ {[Λ := to_lft_stateR bV]}) -∗ ⌜A !! Λ ≡ Some bV⌝.
 Proof.
@@ -57,7 +57,7 @@ Proof.
     + move:Hincl=>/to_agree_included /(inj to_latT)=>HJ. by repeat f_equiv.
 Qed.
 
-Lemma own_bor_auth I κ x : own_ilft_auth I -∗ own_bor κ x -∗ ⌜κ ∈ dom (gset _) I⌝.
+Lemma own_bor_auth I κ x : own_ilft_auth I -∗ own_bor κ x -∗ ⌜κ ∈ dom I⌝.
 Proof.
   iIntros "HI"; iDestruct 1 as (γs) "[? _]".
   by iApply (own_ilft_auth_agree with "HI").
@@ -90,7 +90,7 @@ Proof.
   intros. apply bi.wand_intro_r. rewrite -own_bor_op. by apply own_bor_update.
 Qed.
 
-Lemma own_cnt_auth I κ x : own_ilft_auth I -∗ own_cnt κ x -∗ ⌜κ ∈ dom (gset _) I⌝.
+Lemma own_cnt_auth I κ x : own_ilft_auth I -∗ own_cnt κ x -∗ ⌜κ ∈ dom I⌝.
 Proof.
   iIntros "HI"; iDestruct 1 as (γs) "[? _]".
   by iApply (own_ilft_auth_agree with "HI").
@@ -124,7 +124,7 @@ Proof.
   intros. apply bi.wand_intro_r. rewrite -own_cnt_op. by apply own_cnt_update.
 Qed.
 
-Lemma own_inh_auth I κ x : own_ilft_auth I -∗ own_inh κ x -∗ ⌜κ ∈ dom (gset _) I⌝.
+Lemma own_inh_auth I κ x : own_ilft_auth I -∗ own_inh κ x -∗ ⌜κ ∈ dom I⌝.
 Proof.
   iIntros "HI"; iDestruct 1 as (γs) "[? _]".
   by iApply (own_ilft_auth_agree with "HI").
@@ -165,14 +165,14 @@ Context (A : gmap atomic_lft (bool * Lat)).
 Global Instance lft_alive_in_dec κ : Decision (lft_alive_in A κ).
 Proof.
   refine (cast_if (decide (set_Forall (λ Λ, fst <$> 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 κ : Decision (lft_dead_in A κ).
 Proof.
   refine (cast_if (decide (set_Exists (λ Λ, fst <$> A !! Λ = Some false)
-                  (dom (gset atomic_lft) κ))));
+                  (dom κ))));
       rewrite /lft_dead_in; by setoid_rewrite <-gmultiset_elem_of_dom.
 Qed.
 
@@ -180,9 +180,9 @@ Lemma lft_alive_or_dead_in κ :
   (∃ Λ, Λ ∈ κ ∧ 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 (λ Λ, fst <$> A !! Λ = Some false) (dom (gset _) κ)))
+  destruct (decide (set_Exists (λ Λ, fst <$> 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.
@@ -434,7 +434,7 @@ Proof.
 Qed.
 
 Lemma raw_bor_inI I κ P :
-  ⎡own_ilft_auth I⎤ -∗ raw_bor κ P -∗ ⌜κ ∈ dom (gset _) I⌝.
+  ⎡own_ilft_auth I⎤ -∗ raw_bor κ P -∗ ⌜κ ∈ dom I⌝.
 Proof.
   iIntros "HI Hbor". rewrite /raw_bor /idx_bor_own /=.
   iDestruct "Hbor" as (?) "[Hbor _]". iDestruct "Hbor" as (V) "[_ Hbor]".
@@ -448,7 +448,7 @@ Lemma lft_inh_extend E κ P Q :
      (* This states that κ will henceforth always be allocated.
         That's not at all related to extending the inheritance,
         but it's useful to have it here. *)
-     (∀ I, own_ilft_auth I -∗ ⌜κ ∈ dom (gset _) I⌝) ∗
+     (∀ I, own_ilft_auth I -∗ ⌜κ ∈ dom I⌝) ∗
      (* (* This is the extraction: Always in the future, we can get *)
      (*    â–· P from whatever lft_inh is at the time. *) *)
      (∀ V Q', ▷ lft_inh κ (Some V) Q' ={E}=∗ ∃ Q'',
diff --git a/theories/lifetime/model/reborrow.v b/theories/lifetime/model/reborrow.v
index 19111cb5..15ff1a3c 100644
--- a/theories/lifetime/model/reborrow.v
+++ b/theories/lifetime/model/reborrow.v
@@ -142,7 +142,7 @@ Proof.
   iMod ("Hvs" $! I Vs with "[%] [//] [HI Hinv Hvs' Hinh HB● Hbox HB]
                          [$HPb $Hi] Hκ†") as "($ & $ & Hcnt')"; [solve_lat| |].
   { rewrite lft_vs_inv_unfold. iFrame "HI".
-    iApply (big_sepS_delete _ (dom (gset lft) I) with "[- $Hinv]"); [done|].
+    iApply (big_sepS_delete _ (dom I) with "[- $Hinv]"); [done|].
     iIntros (_). rewrite lft_inv_alive_unfold.
     iExists Pb', Pi'. iFrame "Hvs' Hinh". rewrite /lft_bor_alive.
     iExists (<[i:=Bor_in VP]>B'). rewrite /to_borUR !fmap_insert. iFrame.
@@ -163,7 +163,7 @@ Proof.
   { rewrite /lft_inv_dead. iDestruct "Hinvκ" as (Pi V0) "(>% & Hbordead & H)".
     iMod (raw_bor_fake with "[Hbordead]") as "[Hbordead $]"; [solve_ndisj|by iNext|].
     iMod ("Hclose" with "[-]"); [|done]. iExists _, _. iFrame.
-    rewrite (big_sepS_delete _ (dom _ _) κ') //. iFrame.
+    rewrite (big_sepS_delete _ (dom _) κ') //. iFrame.
     rewrite /lft_inv /lft_inv_dead. iExists _. iFrame "%". iRight. iFrame "%".
     iExists _, _. iFrame "∗%". by iNext. }
   rewrite {1}/raw_bor. iDestruct "Hraw" as (i') "[Hbor H]".
@@ -176,7 +176,7 @@ Proof.
     as %[EQB%to_borUR_included _]%auth_both_valid_discrete.
   iMod (slice_empty _ _ true with "Hs' Hbox") as "[Hidx Hbox]".
   { solve_ndisj. } { by rewrite lookup_fmap EQB. }
-  iAssert (▷ ⌜κ ∈ dom (gset lft) I⌝)%I with "[#]" as ">%".
+  iAssert (▷ ⌜κ ∈ dom I⌝)%I with "[#]" as ">%".
   { iNext. iDestruct (monPred_in_elim with "HV' Hidx") as "Hidx".
     iDestruct "HP'" as "[HP' _]". rewrite /idx_bor_own.
     iDestruct ("HP'" with "Hidx") as (?) "[_ Hown]".
@@ -203,7 +203,7 @@ Proof.
   iDestruct "HH" as "([HI Hinvκ] & Hb & Halive & Hvs)".
   iMod ("Hclose" with "[-Hb]"); last first.
   { iApply (monPred_in_elim with "HV"). by iFrame. }
-  iExists _, _. iFrame. rewrite (big_sepS_delete _ (dom _ _) κ') //.
+  iExists _, _. iFrame. rewrite (big_sepS_delete _ (dom _) κ') //.
   iDestruct ("Hclose'" with "Hinvκ") as "$".
   rewrite /lft_inv. iExists Vκ. iSplit; [done|].
   rewrite lft_inv_alive_unfold. iLeft. iSplit; [|done]. iExists _, _. iFrame.
-- 
GitLab