diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 63aecda5bb352f8557a4e2c08f8172106fd221e4..6c8cdc8997ba6d4a66918ca150dabdbef1d6d2fa 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -27,10 +27,10 @@ variables:
 
 ## Build jobs
 
-build-coq.8.13.0:
+build-coq.8.15.0:
   <<: *template
   variables:
-    OPAM_PINS: "coq version 8.13.0"
+    OPAM_PINS: "coq version 8.15.0"
     OPAM_PKG: "1"
     DENY_WARNINGS: "1"
   tags:
@@ -39,7 +39,7 @@ build-coq.8.13.0:
 build-iris.dev:
   <<: *template
   variables:
-    OPAM_PINS: "coq version 8.13.dev   coq-stdpp.dev git git+https://gitlab.mpi-sws.org/iris/stdpp.git#$STDPP_REV"
+    OPAM_PINS: "coq version 8.15.dev   coq-stdpp.dev git git+https://gitlab.mpi-sws.org/iris/stdpp.git#$STDPP_REV"
   only:
   - triggers
   - schedules
diff --git a/README.md b/README.md
index 5fa668eec91df5a114f235ff886c1e6000e208c0..d84f87cd40b08734284b7018a232610a18d1d57d 100644
--- a/README.md
+++ b/README.md
@@ -7,9 +7,9 @@ Functional Verification of Rust Programs with Unsafe Code".
 
 This version is known to compile with:
 
-- Coq 8.13.0
+- Coq 8.15.0
 - A development version of [Iris](https://gitlab.mpi-sws.org/iris/iris)
-  (the version `dev.2021-03-27.0.f1484b2b`)
+  (the version `dev.2022-04-12.0.a3bed7ea`)
 
 ## Building from source
 
diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index 932a7b90953349601cb8cd277cd32a2908c3091d..aa37621f090100ba1a4cf66898a9e45b5ef650a9 100644
--- a/coq-lambda-rust.opam
+++ b/coq-lambda-rust.opam
@@ -13,8 +13,7 @@ it possible to easily prove the functionnal correctness of well-typed program.
 """
 
 depends: [
-  "coq-iris" { (= "dev.2021-03-27.0.f1484b2b") | (= "dev") }
-  "coq" { (>= "8.13.0") }
+  "coq-iris" { (= "dev.2022-04-12.0.a3bed7ea") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/lang/adequacy.v b/theories/lang/adequacy.v
index 84eda49ae318e6fbc5c5ddd2c9bf7c0e894f4efd..152c5a6a1d0e20222ae48a9df510bc11047c658b 100644
--- a/theories/lang/adequacy.v
+++ b/theories/lang/adequacy.v
@@ -5,22 +5,22 @@ From lrust.lang Require Export heap.
 From lrust.lang Require Import proofmode notation.
 Set Default Proof Using "Type".
 
-Class lrustPreG Σ := HeapPreG {
-  lrust_preG_iris :> invPreG Σ;
-  lrust_preG_heap :> inG Σ (authR heapUR);
-  lrust_preG_heap_freeable :> inG Σ (authR heap_freeableUR);
-  lrust_preG_time :> timePreG Σ
+Class lrustGpreS Σ := HeapGpreS {
+  lrustGpreS_iris :> invGpreS Σ;
+  lrustGpreS_heap :> inG Σ (authR heapUR);
+  lrustGpreS_heap_freeable :> inG Σ (authR heap_freeableUR);
+  lrustGpreS_time :> timePreG Σ
 }.
 
 Definition lrustΣ : gFunctors :=
   #[invΣ; timeΣ;
     GFunctor (constRF (authR heapUR));
     GFunctor (constRF (authR heap_freeableUR))].
-Instance subG_heapPreG {Σ} : subG lrustΣ Σ → lrustPreG Σ.
+Instance subG_heapPreG {Σ} : subG lrustΣ Σ → lrustGpreS Σ.
 Proof. solve_inG. Qed.
 
-Definition lrust_adequacy Σ `{!lrustPreG Σ} e σ φ :
-  (∀ `{!lrustG Σ}, time_ctx -∗ WP e {{ v, ⌜φ v⌝ }}) →
+Definition lrust_adequacy Σ `{!lrustGpreS Σ} e σ φ :
+  (∀ `{!lrustGS Σ}, time_ctx -∗ WP e {{ v, ⌜φ v⌝ }}) →
   adequate NotStuck e σ (λ v _, φ v).
 Proof.
   intros Hwp. apply adequate_alt. intros t2 σ2 [n [κs ?]]%erased_steps_nsteps.
@@ -30,9 +30,9 @@ Proof.
   iMod (own_alloc (● (∅ : heap_freeableUR))) as (fγ) "Hfγ";
     first by apply auth_auth_valid.
   iMod time_init as (Htime) "[TIME Htime]"; [done|].
-  set (Hheap := HeapG _ _ _ vγ fγ).
+  set (Hheap := HeapGS _ _ _ vγ fγ).
   iModIntro. iExists NotStuck, _, [_], _, _. simpl.
-  iDestruct (Hwp (LRustG _ _ Hheap Htime) with "TIME") as "$".
+  iDestruct (Hwp (LRustGS _ _ Hheap Htime) with "TIME") as "$".
   iSplitL; first by auto with iFrame. iIntros ([|e' [|]]? -> ??) "//".
   iIntros "[??] [?_] _". iApply fupd_mask_weaken; [|iIntros "_ !>"]; [done|].
   iSplit; [|done]. iIntros (v2 t2'' [= -> <-]). by rewrite to_of_val.
diff --git a/theories/lang/heap.v b/theories/lang/heap.v
index 19b0c8214f162f9543f3d4ba93fd3194337d0d3b..5fe4d602c5845f877b0bed0a6d16cb3d5ca026ac 100644
--- a/theories/lang/heap.v
+++ b/theories/lang/heap.v
@@ -4,9 +4,9 @@ From iris.algebra Require Import big_op gmap frac agree numbers.
 From iris.algebra Require Import csum excl auth cmra_big_op.
 From iris.bi Require Import fractional.
 From iris.base_logic Require Export lib.own.
-From iris.proofmode Require Export tactics.
+From iris.proofmode Require Export proofmode.
 From lrust.lang Require Export lang.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
 Import uPred.
 
 Definition lock_stateR : cmra :=
@@ -18,7 +18,7 @@ Definition heapUR : ucmra :=
 Definition heap_freeableUR : ucmra :=
   gmapUR block (prodR fracR (gmapR Z (exclR unitO))).
 
-Class heapG Σ := HeapG {
+Class heapGS Σ := HeapGS {
   heap_inG :> inG Σ (authR heapUR);
   heap_freeable_inG :> inG Σ (authR heap_freeableUR);
   heap_name : gname;
@@ -34,7 +34,7 @@ Definition heap_freeable_rel (σ : state) (hF : heap_freeableUR) : Prop :=
     qs.2 ≠ ∅ ∧ ∀ i, is_Some (σ !! (blk, i)) ↔ is_Some (qs.2 !! i).
 
 Section definitions.
-  Context `{!heapG Σ}.
+  Context `{!heapGS Σ}.
 
   Definition heap_mapsto_st (st : lock_state)
              (l : loc) (q : Qp) (v: val) : iProp Σ :=
@@ -42,7 +42,7 @@ Section definitions.
 
   Definition heap_mapsto_def (l : loc) (q : Qp) (v: val) : iProp Σ :=
     heap_mapsto_st (RSt 0) l q v.
-  Definition heap_mapsto_aux : seal (@heap_mapsto_def). by eexists. Qed.
+  Definition heap_mapsto_aux : seal (@heap_mapsto_def). Proof. by eexists. Qed.
   Definition heap_mapsto := unseal heap_mapsto_aux.
   Definition heap_mapsto_eq : @heap_mapsto = @heap_mapsto_def :=
     seal_eq heap_mapsto_aux.
@@ -55,7 +55,7 @@ Section definitions.
 
   Definition heap_freeable_def (l : loc) (q : Qp) (n: nat) : iProp Σ :=
     own heap_freeable_name (◯ {[ l.1 := (q, inter (l.2) n) ]}).
-  Definition heap_freeable_aux : seal (@heap_freeable_def). by eexists. Qed.
+  Definition heap_freeable_aux : seal (@heap_freeable_def). Proof. by eexists. Qed.
   Definition heap_freeable := unseal heap_freeable_aux.
   Definition heap_freeable_eq : @heap_freeable = @heap_freeable_def :=
     seal_eq heap_freeable_aux.
@@ -67,8 +67,8 @@ Section definitions.
 End definitions.
 
 Typeclasses Opaque heap_mapsto heap_freeable heap_mapsto_vec.
-Instance: Params (@heap_mapsto) 4 := {}.
-Instance: Params (@heap_freeable) 5 := {}.
+Global Instance: Params (@heap_mapsto) 4 := {}.
+Global Instance: Params (@heap_freeable) 5 := {}.
 
 Notation "l ↦{ q } v" := (heap_mapsto l q v)
   (at level 20, q at level 50, format "l  ↦{ q }  v") : bi_scope.
@@ -106,7 +106,7 @@ Section to_heap.
 End to_heap.
 
 Section heap.
-  Context `{!heapG Σ}.
+  Context `{!heapGS Σ}.
   Implicit Types P Q : iProp Σ.
   Implicit Types σ : state.
   Implicit Types E : coPset.
@@ -122,7 +122,11 @@ Section heap.
   Qed.
   Global Instance heap_mapsto_as_fractional l q v:
     AsFractional (l ↦{q} v) (λ q, l ↦{q} v)%I q.
-  Proof. split. done. apply _. Qed.
+  Proof. split; first done. apply _. Qed.
+  Global Instance frame_heap_mapsto p l v q1 q2 RES :
+    FrameFractionalHyps p (l ↦{q1} v) (λ q, l ↦{q} v)%I RES q1 q2 →
+    Frame p (l ↦{q1} v) (l ↦{q2} v) RES | 5.
+  Proof. apply: frame_fractional. Qed.
 
   Global Instance heap_mapsto_vec_timeless l q vl : Timeless (l ↦∗{q} vl).
   Proof. rewrite /heap_mapsto_vec. apply _. Qed.
@@ -134,7 +138,11 @@ Section heap.
   Qed.
   Global Instance heap_mapsto_vec_as_fractional l q vl:
     AsFractional (l ↦∗{q} vl) (λ q, l ↦∗{q} vl)%I q.
-  Proof. split. done. apply _. Qed.
+  Proof. split; first done. apply _. Qed.
+  Global Instance frame_heap_mapsto_vec p l vl q1 q2 RES :
+    FrameFractionalHyps p (l ↦∗{q1} vl) (λ q, l ↦∗{q} vl)%I RES q1 q2 →
+    Frame p (l ↦∗{q1} vl) (l ↦∗{q2} vl) RES | 5.
+  Proof. apply: frame_fractional. Qed.
 
   Global Instance heap_freeable_timeless q l n : Timeless (†{q}l…n).
   Proof. rewrite heap_freeable_eq /heap_freeable_def. apply _. Qed.
@@ -243,7 +251,7 @@ Section heap.
   Qed.
   Global Instance heap_mapsto_pred_as_fractional l q (P : list val → iProp Σ):
     (∀ vl, Persistent (P vl)) → AsFractional (l ↦∗{q}: P) (λ q, l ↦∗{q}: P)%I q.
-  Proof. split. done. apply _. Qed.
+  Proof. split; first done. apply _. Qed.
 
   Lemma inter_lookup_Some i j (n : nat):
     i ≤ j < i+n → inter i n !! j = Excl' ().
@@ -266,7 +274,7 @@ Section heap.
     - by rewrite !inter_lookup_None; try lia.
   Qed.
   Lemma inter_valid i n : ✓ inter i n.
-  Proof. revert i. induction n as [|n IH]=>i. done. by apply insert_valid. Qed.
+  Proof. revert i. induction n as [|n IH]=>i; first done. by apply insert_valid. Qed.
 
   Lemma heap_freeable_op_eq l q1 q2 n n' :
     †{q1}l…n ∗ †{q2}l+ₗn … n' ⊣⊢ †{q1+q2}l…(n+n').
@@ -349,7 +357,7 @@ Section heap.
     etrans; first apply (IH (l +ₗ 1)).
     { intros. by rewrite shift_loc_assoc. }
     rewrite shift_loc_0 -insert_singleton_op; last first.
-    { rewrite -equiv_None big_opL_commute equiv_None big_opL_None=> l' v' ?.
+    { rewrite -None_equiv_eq big_opL_commute None_equiv_eq big_opL_None=> l' v' ?.
       rewrite lookup_singleton_None -{2}(shift_loc_0 l). apply not_inj; lia. }
     rewrite to_heap_insert. setoid_rewrite shift_loc_assoc.
     apply alloc_local_update; last done. apply lookup_to_heap_None.
@@ -370,12 +378,13 @@ Section heap.
     { apply auth_update_alloc,
         (alloc_singleton_local_update _ (l.1) (1%Qp, inter (l.2) (Z.to_nat n))).
       - eauto using heap_freeable_rel_None.
-      - split. done. apply inter_valid. }
+      - split; first done. apply inter_valid. }
     iModIntro. iSplitL "Hvalσ HhF".
     { iExists _. iFrame. iPureIntro.
       auto using heap_freeable_rel_init_mem. }
-    rewrite heap_freeable_eq /heap_freeable_def heap_mapsto_vec_combine //.
-    iFrame. destruct (Z.to_nat n); done.
+    rewrite heap_freeable_eq /heap_freeable_def heap_mapsto_vec_combine //; last first.
+    { destruct (Z.to_nat n); done. }
+    iFrame.
   Qed.
 
   Lemma heap_free_vs σ l vl :
@@ -437,7 +446,9 @@ Section heap.
       [/Some_pair_included [_ Hincl] /to_agree_included->].
     destruct ls as [|n], ls'' as [|n''],
        Hincl as [[[|n'|]|] [=]%leibniz_equiv]; subst.
-    by exists O. eauto. exists O. by rewrite Nat.add_0_r.
+    - by exists O.
+    - eauto.
+    - exists O. by rewrite Nat.add_0_r.
   Qed.
 
   Lemma heap_mapsto_lookup_1 σ l ls v :
diff --git a/theories/lang/lib/arc.v b/theories/lang/lib/arc.v
index 86c49cb657333aad0c8688873eb28b857ef70507..8c897d6795c8bcf6a6dd24151edd392d12a9446e 100644
--- a/theories/lang/lib/arc.v
+++ b/theories/lang/lib/arc.v
@@ -1,12 +1,12 @@
 From iris.base_logic.lib Require Import invariants.
 From iris.program_logic Require Import weakestpre.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.bi Require Import fractional.
 From iris.algebra Require Import excl csum frac auth numbers.
 From lrust.lang Require Import lang proofmode notation new_delete.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
 
-(* A: while working on Arc, I think figured that the "weak count
+(* JH: while working on Arc, I think figured that the "weak count
 locking" mechanism that Rust is using and that is verified below may
 not be necessary.
 
@@ -24,7 +24,7 @@ What's wrong with this protocol? The "only" problem I can see is that if
 someone tries to upgrade a weak after we did the CAS, then this will
 fail even though this could be possible.
 
-B: Upgrade failing spuriously sounds like a problem severe enough to
+RJ: Upgrade failing spuriously sounds like a problem severe enough to
 justify the locking protocol.
 *)
 
@@ -99,7 +99,7 @@ Definition try_unwrap_full : val :=
     else #2.
 
 (** The CMRA we need. *)
-(* Not bundling heapG, as it may be shared with other users. *)
+(* Not bundling heapGS, as it may be shared with other users. *)
 
 (* See rc.v for understanding the structure of this CMRA.
    The only additional thing is the [optionR (exclR unitO))], used to handle
@@ -110,11 +110,11 @@ Definition arc_stR :=
 Class arcG Σ :=
   RcG :> inG Σ (authR arc_stR).
 Definition arcΣ : gFunctors := #[GFunctor (authR arc_stR)].
-Instance subG_arcΣ {Σ} : subG arcΣ Σ → arcG Σ.
+Global Instance subG_arcΣ {Σ} : subG arcΣ Σ → arcG Σ.
 Proof. solve_inG. Qed.
 
 Section def.
-  Context `{!lrustG Σ, !arcG Σ} (P1 : Qp → iProp Σ) (P2 : iProp Σ) (N : namespace).
+  Context `{!lrustGS Σ, !arcG Σ} (P1 : Qp → iProp Σ) (P2 : iProp Σ) (N : namespace).
 
   Definition arc_tok γ q : iProp Σ :=
     own γ (◯ (Some $ Cinl (q, 1%positive, None), 0%nat)).
@@ -158,10 +158,10 @@ Section arc.
      this is the lifetime token), and P2 is the thing that is owned by the
      protocol when only weak references are left (in practice, P2 is the
      ownership of the underlying memory incl. deallocation). *)
-  Context `{!lrustG Σ, !arcG Σ} (P1 : Qp → iProp Σ) {HP1:Fractional P1}
+  Context `{!lrustGS Σ, !arcG Σ} (P1 : Qp → iProp Σ) {HP1:Fractional P1}
           (P2 : iProp Σ) (N : namespace).
 
-  Instance P1_AsFractional q : AsFractional (P1 q) P1 q.
+  Local Instance P1_AsFractional q : AsFractional (P1 q) P1 q.
   Proof using HP1. done. Qed.
 
   Global Instance arc_inv_ne n :
@@ -284,7 +284,7 @@ Section arc.
     - wp_apply (wp_cas_int_fail with "Hl"); [congruence|]. iIntros "Hl".
       iMod ("Hclose2" with "Hown") as "HP". iModIntro.
       iMod ("Hclose1" with "[-HP HΦ]") as "_".
-      { iExists _. iFrame. iExists qq. auto with iFrame. }
+      { iExists _. iFrame. iExists qq. iCombine "HP1 HP1'" as "$". auto with iFrame. }
       iModIntro. wp_case. iApply ("IH" with "HP HΦ").
   Qed.
 
@@ -398,7 +398,7 @@ Section arc.
     { iIntros "!> HP". iInv N as (st) "[>H● H]" "Hclose1".
       iMod ("Hacc" with "HP") as "[Hown Hclose2]".
       iDestruct (weak_tok_auth_val with "H● Hown") as %(st' & weak & -> & Hval).
-      destruct st' as [[[[??]?]| |]|]; try done; iExists _.
+      destruct st' as [[[[q' c]?]| |]|]; try done; iExists _.
       - iDestruct "H" as (q) "(>Heq & [HP1 HP1'] & >$ & ?)". iDestruct "Heq" as %Heq.
         iIntros "!>"; iSplit; iMod ("Hclose2" with "Hown") as "HP".
         + iIntros "_ Hl". iExists (q/2)%Qp. iMod (own_update with "H●") as "[H● $]".
@@ -408,10 +408,10 @@ Section arc.
             apply frac_valid. rewrite /= -Heq comm_L.
             by apply Qp_add_le_mono_l, Qp_div_le. }
           iFrame. iApply "Hclose1". iExists _. iFrame. iExists _. iFrame.
-          rewrite /= [xH ⋅ _]comm_L frac_op [(_ + c)%Qp]comm -[(_ + _)%Qp]assoc
+          rewrite /= [xH ⋅ _]comm_L frac_op [(_ + q')%Qp]comm -[(_ + _)%Qp]assoc
                   Qp_div_2 left_id_L. auto with iFrame.
         + iIntros "Hl". iFrame. iApply ("Hclose1" with "[-]"). iExists _. iFrame.
-          iExists q. auto with iFrame.
+          iExists q. iCombine "HP1 HP1'" as "$". auto with iFrame.
       - iDestruct "H" as "[>$ ?]". iIntros "!>"; iSplit; first by auto with congruence.
         iIntros "Hl". iMod ("Hclose2" with "Hown") as "$". iApply "Hclose1".
         iExists _. auto with iFrame.
@@ -521,14 +521,16 @@ Section arc.
           by apply (op_local_update _ _ (Some (Cinr (Excl ())))). }
         iMod ("Hclose" with "[H● Hs Hw]") as "_"; first by iExists _; do 2 iFrame.
         iModIntro. wp_case. iApply wp_fupd. wp_op.
-        iApply ("HΦ"). rewrite -{2}Hq''. iFrame. by iApply close_last_strong.
+        iApply ("HΦ"). rewrite -{2}Hq''. iCombine "HP1 HP1'" as "$".
+        by iApply close_last_strong.
       + destruct Hqq' as [? ->].
         rewrite -[in (_, _)](Pos.succ_pred s) // -[wl in Cinl (_, wl)]left_id
                 -Pos.add_1_l 2!pair_op Cinl_op Some_op.
         iMod (own_update_2 _ _ _ _ with "H● Hown") as "H●".
         { apply auth_update_dealloc, prod_local_update_1, @cancel_local_update_unit, _. }
         iMod ("Hclose" with "[- HΦ]") as "_".
-        { iExists _. iFrame. iExists (q + q'')%Qp. iFrame. iSplit; last by destruct s.
+        { iExists _. iFrame. iExists (q + q'')%Qp. iCombine "HP1 HP1'" as "$".
+          iSplit; last by destruct s.
           iIntros "!> !%". rewrite assoc -Hq''. f_equal. apply comm, _. }
         iModIntro. wp_case. wp_op; case_bool_decide; simplify_eq. by iApply "HΦ".
     - wp_apply (wp_cas_int_fail with "Hs"); [congruence|]. iIntros "Hs".
@@ -553,7 +555,8 @@ Section arc.
         etrans; first apply: cancel_local_update_unit.
         by apply (op_local_update _ _ (Some (Cinr (Excl ())))). }
       iMod ("Hclose" with "[H● Hs Hw]") as "_"; first by iExists _; do 2 iFrame.
-      iApply ("HΦ" $! true). rewrite -{1}Hq''. iFrame. by iApply close_last_strong.
+      iApply ("HΦ" $! true). rewrite -{1}Hq''. iCombine "HP1 HP1'" as "$".
+      by iApply close_last_strong.
     - wp_apply (wp_cas_int_fail with "Hs"); [congruence|]. iIntros "Hs".
       iMod ("Hclose" with "[-Hown HP1 HΦ]") as "_"; first by iExists _; auto with iFrame.
       iApply ("HΦ" $! false). by iFrame.
@@ -597,7 +600,7 @@ Section arc.
         iInv N as ([st w]) "[>H● H]" "Hclose".
         iDestruct (own_valid_2 with "H● H◯") as
            %[[[[=]|Hincl]%option_included _]%prod_included [Hval _]]%auth_both_valid_discrete.
-        simpl in Hincl. destruct Hincl as (? & ? & [=<-] & -> & Hincl); last first.
+        simpl in Hincl. destruct Hincl as (x1 & x2 & [=<-] & -> & Hincl); last first.
         assert (∃ q p, x2 = Cinl (q, p, Excl' ())) as (? & ? & ->).
         { destruct Hincl as [|Hincl]; first by setoid_subst; eauto.
           apply csum_included in Hincl. destruct Hincl as [->|[Hincl|(?&?&[=]&?)]]=>//.
@@ -610,13 +613,13 @@ Section arc.
           csum_local_update_l, prod_local_update_2, delete_option_local_update, _. }
         iMod ("Hclose" with "[-HΦ H◯ HP1]") as "_"; first by iExists _; auto with iFrame.
         iModIntro. wp_seq. iApply "HΦ". iFrame.
-      + setoid_subst. iDestruct "H" as (?) "(Hq & ? & ? & >? & >%)". subst. wp_read.
+      + setoid_subst. iDestruct "H" as (?) "(Hq & HP1' & ? & >? & >%)". subst. wp_read.
         iMod (own_update_2 with "H● H◯") as "H●".
         { apply auth_update_dealloc. rewrite -{1}[(_, 0%nat)]right_id.
           apply cancel_local_update_unit, _. }
         iMod ("Hclose" with "[H●]") as "_"; first by iExists _; iFrame.
         iModIntro. wp_seq. wp_op. wp_let. wp_op. wp_write. iApply "HΦ".
-        iDestruct "Hq" as %<-. iFrame.
+        iDestruct "Hq" as %<-. iCombine "HP1 HP1'" as "$". iFrame.
   Qed.
 
   Lemma try_unwrap_full_spec (γ : gname) (q: Qp) (l : loc) :
diff --git a/theories/lang/lib/lock.v b/theories/lang/lib/lock.v
index ae421b61f2e38d2f8cdd8197bf612fe30761e864..2ab7a9f3f0c0aa08f0cba8b1b8cac26135b43dbf 100644
--- a/theories/lang/lib/lock.v
+++ b/theories/lang/lib/lock.v
@@ -1,5 +1,5 @@
 From iris.program_logic Require Import weakestpre.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.algebra Require Import excl.
 From lrust.lang Require Import lang proofmode notation.
 Set Default Proof Using "Type".
@@ -16,7 +16,7 @@ Definition release : val := λ: ["l"], "l" <-ˢᶜ #false.
    their cancelling view shift has a non-empty mask, and it would have to be
    executed in the consequence view shift of a borrow. *)
 Section proof.
-  Context `{!lrustG Σ}.
+  Context `{!lrustGS Σ}.
 
   Definition lock_proto (l : loc) (R : iProp Σ) : iProp Σ :=
     (∃ b : bool, l ↦ #b ∗ if b then True else R)%I.
diff --git a/theories/lang/lib/memcpy.v b/theories/lang/lib/memcpy.v
index 59272fd59caee3b9e3112bbe32cbee2ddb21e9a0..cdb8058e3931da25a26fc32464716776ee9858bb 100644
--- a/theories/lang/lib/memcpy.v
+++ b/theories/lang/lib/memcpy.v
@@ -16,7 +16,7 @@ Notation "e1 <-{ n ',Σ' i } ! e2" :=
   (e1%E%E <- #(LitInt i);; e1 +ₗ #(LitInt 1) <-{n} !e2)%E
   (at level 80, n, i at next level, format "e1  <-{ n ,Σ  i }  ! e2") : expr_scope.
 
-Lemma wp_memcpy `{!lrustG Σ} E l1 l2 vl1 vl2 q (n : Z):
+Lemma wp_memcpy `{!lrustGS Σ} E l1 l2 vl1 vl2 q (n : Z):
   Z.of_nat (length vl1) = n → Z.of_nat (length vl2) = n →
   {{{ l1 ↦∗ vl1 ∗ l2 ↦∗{q} vl2 }}}
     #l1 <-{n} !#l2 @ E
diff --git a/theories/lang/lib/new_delete.v b/theories/lang/lib/new_delete.v
index d1db9df5fb40205c12d715d0a0b9a6c40a322615..4d4dbd6907321299bc945f8d13636fef5a1ed617 100644
--- a/theories/lang/lib/new_delete.v
+++ b/theories/lang/lib/new_delete.v
@@ -13,7 +13,7 @@ Definition delete : val :=
     else Free "n" "loc".
 
 Section specs.
-  Context `{!lrustG Σ}.
+  Context `{!lrustGS Σ}.
 
   Lemma wp_new E n:
     0 ≤ n →
diff --git a/theories/lang/lib/spawn.v b/theories/lang/lib/spawn.v
index 55feed47684cd7ab003735cea52441fc0f52bae2..66ad5d229099a19ad7fcb1a0903d8fc67c96fcdd 100644
--- a/theories/lang/lib/spawn.v
+++ b/theories/lang/lib/spawn.v
@@ -1,6 +1,6 @@
 From iris.program_logic Require Import weakestpre.
 From iris.base_logic.lib Require Import invariants.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.algebra Require Import excl.
 From lrust.lang Require Import proofmode notation.
 From lrust.lang Require Export lang.
@@ -36,7 +36,7 @@ Proof. solve_inG. Qed.
 
 (** Now we come to the Iris part of the proof. *)
 Section proof.
-Context `{!lrustG Σ, !spawnG Σ} (N : namespace).
+Context `{!lrustGS Σ, !spawnG Σ} (N : namespace).
 
 Definition spawn_inv (γf γj : gname) (c : loc) (Ψ : val → iProp Σ) : iProp Σ :=
   (own γf (Excl ()) ∗ own γj (Excl ()) ∨
diff --git a/theories/lang/lib/swap.v b/theories/lang/lib/swap.v
index d182c900cf72ad3248326c888b4343540b8c047b..e6997bbe414128c467d5869ef3ac08783f4c7421 100644
--- a/theories/lang/lib/swap.v
+++ b/theories/lang/lib/swap.v
@@ -10,7 +10,7 @@ Definition swap : val :=
          "p2" <- "x";;
          "swap" ["p1" +ₗ #1 ; "p2" +ₗ #1 ; "len" - #1].
 
-Lemma wp_swap `{!lrustG Σ} E l1 l2 vl1 vl2 (n : Z):
+Lemma wp_swap `{!lrustGS Σ} E l1 l2 vl1 vl2 (n : Z):
   Z.of_nat (length vl1) = n → Z.of_nat (length vl2) = n →
   {{{ l1 ↦∗ vl1 ∗ l2 ↦∗ vl2 }}}
     swap [ #l1; #l2; #n] @ E
diff --git a/theories/lang/lib/tests.v b/theories/lang/lib/tests.v
index 8f414deb52aa61ec33e4e20b76385cd83febbc64..7f6ebbaa0151d64058862dab062f01b6dec2ec40 100644
--- a/theories/lang/lib/tests.v
+++ b/theories/lang/lib/tests.v
@@ -1,10 +1,10 @@
 From iris.program_logic Require Import weakestpre.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From lrust.lang Require Import lang proofmode notation.
 Set Default Proof Using "Type".
 
 Section tests.
-  Context `{!lrustG Σ}.
+  Context `{!lrustGS Σ}.
 
   Lemma test_location_cmp E (l1 l2 : loc) q1 q2 v1 v2 :
     {{{ ▷ l1 ↦{q1} v1 ∗ ▷ l2 ↦{q2} v2 }}}
diff --git a/theories/lang/lifting.v b/theories/lang/lifting.v
index 1ccf972c54b23eac4d5cd897b3b0bd26907a0a8a..844d971d9483ee9f6c6465844393e9b9e7481ade 100644
--- a/theories/lang/lifting.v
+++ b/theories/lang/lifting.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.program_logic Require Export weakestpre.
 From iris.program_logic Require Import ectx_lifting.
 From lrust.lang Require Export lang heap time.
@@ -6,14 +6,14 @@ From lrust.lang Require Import tactics.
 Set Default Proof Using "Type".
 Import uPred.
 
-Class lrustG Σ := LRustG {
-  lrustG_invG : invG Σ;
-  lrustG_gen_heapG :> heapG Σ;
-  lrustG_gen_timeG :> timeG Σ
+Class lrustGS Σ := LRustGS {
+  lrustGS_invGS : invGS Σ;
+  lrustGS_gen_heapGS :> heapGS Σ;
+  lrustGS_gen_timeGS :> timeGS Σ
 }.
 
-Program Instance lrustG_irisG `{!lrustG Σ} : irisG lrust_lang Σ := {
-  iris_invG := lrustG_invG;
+Program Instance lrustGS_irisGS `{!lrustGS Σ} : irisGS lrust_lang Σ := {
+  iris_invGS := lrustGS_invGS;
   state_interp σ stepcnt κs _ := (heap_ctx σ ∗ time_interp stepcnt)%I;
   fork_post _ := True%I;
   num_laters_per_step n := n
@@ -22,7 +22,7 @@ Next Obligation.
   intros. iIntros "/= [$ H]". by iMod (time_interp_step with "H") as "$".
 Qed.
 
-Global Opaque iris_invG.
+Global Opaque iris_invGS.
 
 Ltac inv_lit :=
   repeat match goal with
@@ -67,7 +67,7 @@ Instance do_subst_vec xl (vsl : vec val (length xl)) e :
 Proof. by rewrite /DoSubstL subst_v_eq. Qed.
 
 Section lifting.
-Context `{!lrustG Σ}.
+Context `{!lrustGS Σ}.
 Implicit Types P Q : iProp Σ.
 Implicit Types e : expr.
 Implicit Types ef : option expr.
diff --git a/theories/lang/proofmode.v b/theories/lang/proofmode.v
index 386756f24584892d2e321d9391d73190d805b5bb..14b227b6e0998c12cb155ea0a4631bcd8de972a4 100644
--- a/theories/lang/proofmode.v
+++ b/theories/lang/proofmode.v
@@ -6,14 +6,14 @@ From lrust.lang Require Export tactics lifting.
 Set Default Proof Using "Type".
 Import uPred.
 
-Lemma tac_wp_value `{!lrustG Σ} Δ E Φ e v :
+Lemma tac_wp_value `{!lrustGS Σ} Δ E Φ e v :
   IntoVal e v →
   envs_entails Δ (Φ v) → envs_entails Δ (WP e @ E {{ Φ }}).
 Proof. rewrite envs_entails_eq=> ? ->. by apply wp_value. Qed.
 
 Ltac wp_value_head := eapply tac_wp_value; [iSolveTC|reduction.pm_prettify].
 
-Lemma tac_wp_pure `{!lrustG Σ} K Δ Δ' E e1 e2 φ n Φ :
+Lemma tac_wp_pure `{!lrustGS Σ} K Δ Δ' E e1 e2 φ n Φ :
   PureExec φ n e1 e2 →
   φ →
   MaybeIntoLaterNEnvs n Δ Δ' →
@@ -38,7 +38,7 @@ Tactic Notation "wp_pure" open_constr(efoc) :=
   | _ => fail "wp_pure: not a 'wp'"
   end.
 
-Lemma tac_wp_eq_loc `{!lrustG Σ} K Δ Δ' E i1 i2 l1 l2 q1 q2 v1 v2 Φ :
+Lemma tac_wp_eq_loc `{!lrustGS Σ} K Δ Δ' E i1 i2 l1 l2 q1 q2 v1 v2 Φ :
   MaybeIntoLaterNEnvs 1 Δ Δ' →
   envs_lookup i1 Δ' = Some (false, l1 ↦{q1} v1)%I →
   envs_lookup i2 Δ' = Some (false, l2 ↦{q2} v2)%I →
@@ -67,7 +67,7 @@ Tactic Notation "wp_op" := wp_pure (BinOp _ _ _) || wp_eq_loc.
 Tactic Notation "wp_if" := wp_pure (If _ _ _).
 Tactic Notation "wp_case" := wp_pure (Case _ _); try wp_value_head.
 
-Lemma tac_wp_bind `{!lrustG Σ} K Δ E Φ e :
+Lemma tac_wp_bind `{!lrustGS Σ} K Δ E Φ e :
   envs_entails Δ (WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }})%I →
   envs_entails Δ (WP fill K e @ E {{ Φ }}).
 Proof. rewrite envs_entails_eq=> ->. apply: wp_bind. Qed.
@@ -89,12 +89,12 @@ Tactic Notation "wp_bind" open_constr(efoc) :=
   end.
 
 Section heap.
-Context `{!lrustG Σ}.
+Context `{!lrustGS Σ}.
 Implicit Types P Q : iProp Σ.
 Implicit Types Φ : val → iProp Σ.
 Implicit Types Δ : envs (uPredI (iResUR Σ)).
 
-Lemma tac_wp_nd_int `{!lrustG Σ} K Δ Δ' E Φ :
+Lemma tac_wp_nd_int `{!lrustGS Σ} K Δ Δ' E Φ :
   MaybeIntoLaterNEnvs 1 Δ Δ' →
   (∀z, envs_entails Δ' (WP fill K (Lit (LitInt z)) @ E {{ Φ }})) →
   envs_entails Δ (WP fill K NdInt @ E {{ Φ }}).
diff --git a/theories/lang/time.v b/theories/lang/time.v
index f7532a6a995f3a0e4cc76628284e449e9914541a..3e26718a50c2c0135021920e93f90816526de35e 100644
--- a/theories/lang/time.v
+++ b/theories/lang/time.v
@@ -1,12 +1,12 @@
 From iris.algebra Require Import lib.mono_nat numbers.
 From iris.base_logic Require Import lib.own.
 From iris.base_logic.lib Require Export invariants.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From lrust.lang Require Export lang.
 Set Default Proof Using "Type".
 Import uPred.
 
-Class timeG Σ := TimeG {
+Class timeGS Σ := TimeG {
   time_mono_nat_inG :> inG Σ mono_natR;
   time_nat_inG :> inG Σ (authR natUR);
   time_global_name : gname;
@@ -27,7 +27,7 @@ Proof. solve_inG. Qed.
 Definition timeN : namespace := nroot .@ "lft_usr" .@ "time".
 
 Section definitions.
-  Context `{!timeG Σ}.
+  Context `{!timeGS Σ}.
 
   (** persistent time receipt *)
   Definition persistent_time_receipt (n : nat) :=
@@ -36,19 +36,19 @@ Section definitions.
   Definition cumulative_time_receipt (n : nat) :=
     own time_cumulative_name (◯ n).
   (** invariant *)
-  Definition time_ctx `{!invG Σ} :=
+  Definition time_ctx `{!invGS Σ} :=
     inv timeN (∃ n m,
        own time_global_name (mono_nat_lb (n + m)) ∗
        own time_cumulative_name (● n) ∗
-       own time_persistent_name (mono_nat_auth 1 m)).
+       own time_persistent_name (●MN m)).
   (** authority *)
   Definition time_interp (n: nat) : iProp Σ :=
-    own time_global_name (mono_nat_auth 1 n).
+    own time_global_name (●MN n).
 End definitions.
 
-Typeclasses Opaque persistent_time_receipt cumulative_time_receipt.
-Instance: Params (@persistent_time_receipt) 2 := {}.
-Instance: Params (@cumulative_time_receipt) 2 := {}.
+Global Typeclasses Opaque persistent_time_receipt cumulative_time_receipt.
+Global Instance: Params (@persistent_time_receipt) 2 := {}.
+Global Instance: Params (@cumulative_time_receipt) 2 := {}.
 
 Notation "⧖ n" := (persistent_time_receipt n)
   (at level 1, format "⧖ n") : bi_scope.
@@ -56,7 +56,7 @@ Notation "⧗ n" := (cumulative_time_receipt n)
   (at level 1, format "⧗ n") : bi_scope.
 
 Section time.
-  Context `{!timeG Σ}.
+  Context `{!timeGS Σ}.
   Implicit Types P Q : iProp Σ.
 
   Global Instance persistent_time_receipt_timeless n : Timeless (⧖n).
@@ -83,7 +83,7 @@ Section time.
   Qed.
 
   Lemma persistent_time_receipt_sep n m : ⧖(n `max` m) ⊣⊢ ⧖n ∗ ⧖m.
-  Proof. by rewrite /persistent_time_receipt -mono_nat_lb_op own_op. Qed.
+  Proof. by rewrite /persistent_time_receipt mono_nat_lb_op own_op. Qed.
   Lemma cumulative_time_receipt_sep n m : ⧗(n + m) ⊣⊢ ⧗n ∗ ⧗m.
   Proof. by rewrite /cumulative_time_receipt -nat_op auth_frag_op own_op. Qed.
 
@@ -101,7 +101,7 @@ Section time.
   Lemma cumulative_time_receipt_0 : ⊢ |==> ⧗0.
   Proof. rewrite /cumulative_time_receipt. apply own_unit. Qed.
 
-  Lemma cumulative_persistent_time_receipt `{!invG Σ} E n m :
+  Lemma cumulative_persistent_time_receipt `{!invGS Σ} E n m :
     ↑timeN ⊆ E → time_ctx -∗ ⧗n -∗ ⧖m ={E}=∗ ⧖(n + m).
   Proof.
     iIntros (?) "#TIME Hn #Hm".
@@ -121,7 +121,7 @@ Section time.
     rewrite (_:(n'+m')%nat = ((n'-n) + (m'+n))%nat); [done|lia].
   Qed.
 
-  Lemma step_cumulative_time_receipt `{!invG Σ} E n :
+  Lemma step_cumulative_time_receipt `{!invGS Σ} E n :
     ↑timeN ⊆ E →
     time_ctx -∗ time_interp n ={E, E∖↑timeN}=∗ time_interp n ∗
     (time_interp (S n) ={E∖↑timeN, E}=∗ time_interp (S n) ∗ ⧗1).
@@ -137,7 +137,7 @@ Section time.
     iApply (own_mono with "H'Sn"). apply mono_nat_lb_mono. lia.
   Qed.
 
-  Lemma time_receipt_le `{!invG Σ} E n m m' :
+  Lemma time_receipt_le `{!invGS Σ} E n m m' :
     ↑timeN ⊆ E →
     time_ctx -∗ time_interp n -∗ ⧖m -∗ ⧗m' ={E}=∗
     ⌜m+m' ≤ n⌝%nat ∗ time_interp n ∗ ⧗m'.
@@ -151,13 +151,13 @@ Section time.
   Qed.
 End time.
 
-Lemma time_init `{!invG Σ, !timePreG Σ} E : ↑timeN ⊆ E →
-  ⊢ |={E}=> ∃ _ : timeG Σ, time_ctx ∗ time_interp 0.
+Lemma time_init `{!invGS Σ, !timePreG Σ} E : ↑timeN ⊆ E →
+  ⊢ |={E}=> ∃ _ : timeGS Σ, time_ctx ∗ time_interp 0.
 Proof.
   intros ?.
-  iMod (own_alloc (mono_nat_auth 1 0 ⋅ mono_nat_lb 0)) as (time_global_name) "[??]";
+  iMod (own_alloc (●MN 0 ⋅ mono_nat_lb 0)) as (time_global_name) "[??]";
     [by apply mono_nat_both_valid|].
-  iMod (own_alloc (mono_nat_auth 1 0)) as (time_persistent_name) "?";
+  iMod (own_alloc (●MN 0)) as (time_persistent_name) "?";
     [by apply mono_nat_auth_valid|].
   iMod (own_alloc (● 0%nat)) as (time_cumulative_name) "?"; [by apply auth_auth_valid|].
   iExists (TimeG _ _ _ time_global_name time_persistent_name time_cumulative_name).
diff --git a/theories/lifetime/at_borrow.v b/theories/lifetime/at_borrow.v
index 0c9d3409bcf51bf25226e47832f77edad5253b85..091ab8839de87cbbd3ecc752f818a50fe932119e 100644
--- a/theories/lifetime/at_borrow.v
+++ b/theories/lifetime/at_borrow.v
@@ -5,14 +5,14 @@ Set Default Proof Using "Type".
 
 (** Atomic persistent bors  *)
 (* TODO : update the TEX with the fact that we can choose the namespace. *)
-Definition at_bor `{!invG Σ, !lftG Σ} κ N (P : iProp Σ) :=
+Definition at_bor `{!invGS Σ, !lftGS Σ} κ N (P : iProp Σ) :=
   (∃ i, &{κ,i}P ∗
     (⌜N ## lftN⌝ ∗ inv N (idx_bor_own 1 i) ∨
      ⌜N = lftN⌝ ∗ inv N (∃ q, idx_bor_own q i)))%I.
 Notation "&at{ κ , N }" := (at_bor κ N) (format "&at{ κ , N }") : bi_scope.
 
 Section atomic_bors.
-  Context `{!invG Σ, !lftG Σ} (P : iProp Σ) (N : namespace).
+  Context `{!invGS Σ, !lftGS Σ} (P : iProp Σ) (N : namespace).
 
   Global Instance at_bor_ne κ n : Proper (dist n ==> dist n) (at_bor κ N).
   Proof. solve_proper. Qed.
@@ -97,7 +97,7 @@ Section atomic_bors.
   Qed.
 End atomic_bors.
 
-Lemma at_bor_acc_lftN `{!invG Σ, !lftG Σ} (P : iProp Σ) E κ :
+Lemma at_bor_acc_lftN `{!invGS Σ, !lftGS Σ} (P : iProp Σ) E κ :
   ↑lftN ⊆ E →
   lft_ctx -∗ &at{κ,lftN}P ={E,E∖↑lftN}=∗ ▷P ∗ (▷P ={E∖↑lftN,E}=∗ True) ∨
              [†κ] ∗ |={E∖↑lftN,E}=> True.
diff --git a/theories/lifetime/frac_borrow.v b/theories/lifetime/frac_borrow.v
index 8936fa117f998a4c398379f9305c4dd1921c67e6..d04759524e2a67772842e8ab3dd9213872b0d819 100644
--- a/theories/lifetime/frac_borrow.v
+++ b/theories/lifetime/frac_borrow.v
@@ -6,15 +6,15 @@ Set Default Proof Using "Type".
 
 Class frac_borG Σ := frac_borG_inG :> inG Σ fracR.
 
-Local Definition frac_bor_inv `{!invG Σ, !lftG Σ, !frac_borG Σ} (φ : Qp → iProp Σ) γ κ' :=
+Local Definition frac_bor_inv `{!invGS Σ, !lftGS Σ, !frac_borG Σ} (φ : Qp → iProp Σ) γ κ' :=
   (∃ q, φ q ∗ own γ q ∗ (⌜q = 1%Qp⌝ ∨ ∃ q', ⌜(q + q' = 1)%Qp⌝ ∗ q'.[κ']))%I.
 
-Definition frac_bor `{!invG Σ, !lftG Σ, !frac_borG Σ} κ (φ : Qp → iProp Σ) :=
+Definition frac_bor `{!invGS Σ, !lftGS Σ, !frac_borG Σ} κ (φ : Qp → iProp Σ) :=
   (∃ γ κ', κ ⊑ κ' ∗ &at{κ',lftN} (frac_bor_inv φ γ κ'))%I.
 Notation "&frac{ κ }" := (frac_bor κ) (format "&frac{ κ }") : bi_scope.
 
 Section frac_bor.
-  Context `{!invG Σ, !lftG Σ, !frac_borG Σ} (φ : Qp → iProp Σ).
+  Context `{!invGS Σ, !lftGS Σ, !frac_borG Σ} (φ : Qp → iProp Σ).
   Implicit Types E : coPset.
 
   Global Instance frac_bor_contractive κ n :
@@ -108,8 +108,8 @@ Section frac_bor.
       - iRight. iExists qq. iFrame. iPureIntro.
         by rewrite (comm _ qφ0).
       - iDestruct "Hq" as (q') "[% Hq'κ]". iRight. iExists (qq + q')%Qp.
-        iFrame. iPureIntro.
-        rewrite assoc (comm _ _ qq). done.
+        iSplitR; last first. { iApply fractional_split. iFrame. }
+        iPureIntro. rewrite assoc (comm _ _ qq). done.
   Qed.
 
   Lemma frac_bor_acc' E q κ :
@@ -129,7 +129,8 @@ Section frac_bor.
     iMod (at_bor_acc_tok with "LFT Hshr Hκ1") as "[H Hclose']"; try done.
     iDestruct (frac_bor_trade1 with "Hφ [$H $Hown $Hqφ]") as "[H >Hκ3]".
     iMod ("Hclose'" with "H") as "Hκ1".
-    iApply "Hclose". iFrame "Hκ1". rewrite Hq. iFrame.
+    iApply "Hclose". iApply fractional_half. iFrame "Hκ1". rewrite Hq.
+    iApply fractional_split. iFrame.
   Qed.
 
   Lemma frac_bor_acc E q κ `{!Fractional φ} :
@@ -154,7 +155,7 @@ Section frac_bor.
   Qed.
 End frac_bor.
 
-Lemma frac_bor_lft_incl `{!invG Σ, !lftG Σ, !frac_borG Σ} κ κ' q:
+Lemma frac_bor_lft_incl `{!invGS Σ, !lftGS Σ, !frac_borG Σ} κ κ' q:
   lft_ctx -∗ &frac{κ}(λ q', (q * q').[κ']) -∗ κ ⊑ κ'.
 Proof.
   iIntros "#LFT#Hbor". iApply lft_incl_intro. iModIntro. iSplitR.
diff --git a/theories/lifetime/lifetime.v b/theories/lifetime/lifetime.v
index 47b85f69b82115c46289209380e116b4039705d0..a184733fc178dcb88da6b799cee732b994930509 100644
--- a/theories/lifetime/lifetime.v
+++ b/theories/lifetime/lifetime.v
@@ -30,12 +30,12 @@ Instance lft_inhabited : Inhabited lft := populate static.
 
 Canonical lftO := leibnizO lft.
 
-Definition lft_equiv `{!invG Σ, !lftG Σ} (κ κ':lft) : iProp Σ :=
+Definition lft_equiv `{!invGS Σ, !lftGS Σ} (κ κ':lft) : iProp Σ :=
   κ ⊑ κ' ∗ κ' ⊑ κ.
 Infix "≡ₗ" := lft_equiv (at level 70) : bi_scope.
 
 Section derived.
-Context `{!invG Σ, !lftG Σ}.
+Context `{!invGS Σ, !lftGS Σ}.
 Implicit Types κ : lft.
 
 (* Deriving this just to prove that it can be derived.
diff --git a/theories/lifetime/lifetime_sig.v b/theories/lifetime/lifetime_sig.v
index 36cff7626d645103a9b752ccd91ed41789b35250..5f94a63cffb005623b2cfd3de6b9c55fe137399b 100644
--- a/theories/lifetime/lifetime_sig.v
+++ b/theories/lifetime/lifetime_sig.v
@@ -3,6 +3,7 @@ From stdpp Require Export gmultiset strings.
 From iris.base_logic.lib Require Export invariants.
 From iris.base_logic.lib Require Import boxes.
 From iris.bi Require Import fractional.
+From iris.proofmode Require Import proofmode.
 Set Default Proof Using "Type".
 
 Definition lftN : namespace := nroot .@ "lft".
@@ -14,29 +15,29 @@ Module Type lifetime_sig.
   (** CMRAs needed by the lifetime logic  *)
   (* We can't instantie the module parameters with inductive types, so we
      have aliases here. *)
-  Parameter lftG' : gFunctors → Set.
-  Global Notation lftG := lftG'.
-  Existing Class lftG'.
-  Parameter lftPreG' : gFunctors → Set.
-  Global Notation lftPreG := lftPreG'.
-  Existing Class lftPreG'.
+  Parameter lftGS' : gFunctors → Set.
+  Global Notation lftGS := lftGS'.
+  Existing Class lftGS'.
+  Parameter lftGpreS' : gFunctors → Set.
+  Global Notation lftGpreS := lftGpreS'.
+  Existing Class lftGpreS'.
 
   (** Definitions *)
   Parameter lft : Type.
   Parameter static : lft.
   Declare Instance lft_intersect : Meet lft.
 
-  Parameter lft_ctx : ∀ `{!invG Σ, !lftG Σ}, iProp Σ.
+  Parameter lft_ctx : ∀ `{!invGS Σ, !lftGS Σ}, iProp Σ.
 
-  Parameter lft_tok : ∀ `{!lftG Σ} (q : Qp) (κ : lft), iProp Σ.
-  Parameter lft_dead : ∀ `{!lftG Σ} (κ : lft), iProp Σ.
+  Parameter lft_tok : ∀ `{!lftGS Σ} (q : Qp) (κ : lft), iProp Σ.
+  Parameter lft_dead : ∀ `{!lftGS Σ} (κ : lft), iProp Σ.
 
-  Parameter lft_incl : ∀ `{!invG Σ, !lftG Σ} (κ κ' : lft), iProp Σ.
-  Parameter bor : ∀ `{!invG Σ, !lftG Σ} (κ : lft) (P : iProp Σ), iProp Σ.
+  Parameter lft_incl : ∀ `{!invGS Σ, !lftGS Σ} (κ κ' : lft), iProp Σ.
+  Parameter bor : ∀ `{!invGS Σ, !lftGS Σ} (κ : lft) (P : iProp Σ), iProp Σ.
 
   Parameter bor_idx : Type.
-  Parameter idx_bor_own : ∀ `{!lftG Σ} (q : frac) (i : bor_idx), iProp Σ.
-  Parameter idx_bor : ∀ `{!invG Σ, !lftG Σ} (κ : lft) (i : bor_idx) (P : iProp Σ), iProp Σ.
+  Parameter idx_bor_own : ∀ `{!lftGS Σ} (q : frac) (i : bor_idx), iProp Σ.
+  Parameter idx_bor : ∀ `{!invGS Σ, !lftGS Σ} (κ : lft) (i : bor_idx) (P : iProp Σ), iProp Σ.
 
   (** Notation *)
   Notation "q .[ κ ]" := (lft_tok q κ)
@@ -49,7 +50,7 @@ Module Type lifetime_sig.
   Infix "⊑" := lft_incl (at level 70) : bi_scope.
 
   Section properties.
-  Context `{!invG Σ, !lftG Σ}.
+  Context `{!invGS Σ, !lftGS Σ}.
 
   (** Instances *)
   Global Declare Instance lft_inhabited : Inhabited lft.
@@ -84,9 +85,16 @@ Module Type lifetime_sig.
   Global Declare Instance lft_tok_fractional κ : Fractional (λ q, q.[κ])%I.
   Global Declare Instance lft_tok_as_fractional κ q :
     AsFractional q.[κ] (λ q, q.[κ])%I q.
+  Global Declare Instance frame_lft_tok p κ q1 q2 RES :
+    FrameFractionalHyps p q1.[κ] (λ q, q.[κ])%I RES q1 q2 →
+    Frame p q1.[κ] q2.[κ] RES | 5.
+
   Global Declare Instance idx_bor_own_fractional i : Fractional (λ q, idx_bor_own q i)%I.
   Global Declare Instance idx_bor_own_as_fractional i q :
     AsFractional (idx_bor_own q i) (λ q, idx_bor_own q i)%I q.
+  Global Declare Instance frame_idx_bor_own p i q1 q2 RES :
+    FrameFractionalHyps p (idx_bor_own q1 i) (λ q, idx_bor_own q i)%I RES q1 q2 →
+    Frame p (idx_bor_own q1 i) (idx_bor_own q2 i) RES | 5.
 
   (** Laws *)
   Parameter lft_tok_sep : ∀ q κ1 κ2, q.[κ1] ∗ q.[κ2] ⊣⊢ q.[κ1 ⊓ κ2].
@@ -158,8 +166,8 @@ Module Type lifetime_sig.
   End properties.
 
   Parameter lftΣ : gFunctors.
-  Global Declare Instance subG_lftPreG Σ : subG lftΣ Σ → lftPreG Σ.
+  Global Declare Instance subG_lftGpreS Σ : subG lftΣ Σ → lftGpreS Σ.
 
-  Parameter lft_init : ∀ `{!invG Σ, !lftPreG Σ} E, ↑lftN ⊆ E →
-    ⊢ |={E}=> ∃ _ : lftG Σ, lft_ctx.
+  Parameter lft_init : ∀ `{!invGS Σ, !lftGpreS Σ} E, ↑lftN ⊆ E →
+    ⊢ |={E}=> ∃ _ : lftGS Σ, lft_ctx.
 End lifetime_sig.
diff --git a/theories/lifetime/model/accessors.v b/theories/lifetime/model/accessors.v
index dab4be3c7c7b1d7eb4ba937f57867ea448e8b2ab..ff73ee3237cecb5a3ac514529580ff2cf66416cf 100644
--- a/theories/lifetime/model/accessors.v
+++ b/theories/lifetime/model/accessors.v
@@ -5,7 +5,7 @@ From iris.base_logic.lib Require Import boxes.
 Set Default Proof Using "Type".
 
 Section accessors.
-Context `{!invG Σ, !lftG Σ}.
+Context `{!invGS Σ, !lftGS Σ}.
 Implicit Types κ : lft.
 
 (* Helper internal lemmas *)
@@ -28,7 +28,7 @@ Proof.
     by apply (exclusive_local_update _ (1%Qp, to_agree (Bor_open q))). }
   rewrite own_bor_op -fmap_insert. iDestruct "Hbor" as "[Hown $]".
   iExists _. iFrame "∗".
-  rewrite -insert_delete big_sepM_insert ?lookup_delete // big_sepM_delete /=; last done.
+  rewrite -insert_delete_insert big_sepM_insert ?lookup_delete // big_sepM_delete /=; last done.
   iDestruct "HB" as "[_ $]". auto.
 Qed.
 
@@ -51,7 +51,7 @@ Proof.
   rewrite own_bor_op -fmap_insert. iDestruct "Hbor" as "[Hown $]".
   rewrite big_sepM_delete //. simpl. iDestruct "HB" as "[>$ HB]".
   iExists _. iFrame "Hbox Hown".
-  rewrite -insert_delete big_sepM_insert ?lookup_delete //. simpl. by iFrame.
+  rewrite -insert_delete_insert big_sepM_insert ?lookup_delete //. simpl. by iFrame.
 Qed.
 
 Lemma add_vs Pb Pb' P Q Pi κ :
diff --git a/theories/lifetime/model/borrow.v b/theories/lifetime/model/borrow.v
index 03ff321de45284ee6170d7c1f25ceb01f33b93e7..d12f215b744833b5b61866bea5eb9835d7c237e8 100644
--- a/theories/lifetime/model/borrow.v
+++ b/theories/lifetime/model/borrow.v
@@ -6,7 +6,7 @@ From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 
 Section borrow.
-Context `{!invG Σ, !lftG Σ}.
+Context `{!invGS Σ, !lftGS Σ}.
 Implicit Types κ : lft.
 
 Lemma raw_bor_create E κ P :
diff --git a/theories/lifetime/model/borrow_sep.v b/theories/lifetime/model/borrow_sep.v
index 3a4348e8339d3018f178b3d7bf39f9090bdadd9c..c961c6179c5a1cbdf17a525fd32fc94f0228bf25 100644
--- a/theories/lifetime/model/borrow_sep.v
+++ b/theories/lifetime/model/borrow_sep.v
@@ -6,7 +6,7 @@ From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 
 Section borrow.
-Context `{!invG Σ, !lftG Σ}.
+Context `{!invGS Σ, !lftGS Σ}.
 Implicit Types κ : lft.
 
 Lemma bor_sep E κ P Q :
diff --git a/theories/lifetime/model/creation.v b/theories/lifetime/model/creation.v
index bf215b53979ee7017984228aac59b5122694b8fb..f6e00a1b649c331cc766e1ea36509b41a73947b9 100644
--- a/theories/lifetime/model/creation.v
+++ b/theories/lifetime/model/creation.v
@@ -6,7 +6,7 @@ From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 
 Section creation.
-Context `{!invG Σ, !lftG Σ}.
+Context `{!invGS Σ, !lftGS Σ}.
 Implicit Types κ : lft.
 
 Lemma lft_kill (I : gmap lft lft_names) (K K' : gset lft) (κ : lft) :
@@ -125,7 +125,7 @@ Proof.
     iModIntro. rewrite /lft_inv. iIntros (κ ?) "[[Hκ %]|[Hκ %]]".
     - iLeft. iFrame "Hκ". iPureIntro. by apply lft_alive_in_insert.
     - iRight. iFrame "Hκ". iPureIntro. by apply lft_dead_in_insert. }
-  iModIntro; iExists {[ Λ ]}.
+  iModIntro; iExists {[+ Λ +]}.
   rewrite {1}/lft_tok big_sepMS_singleton. iFrame "HΛ".
   clear I A HΛ. iIntros "!> HΛ".
   iApply (step_fupd_mask_mono (↑lftN ∪ ↑lft_userN) _ ((↑lftN ∪ ↑lft_userN)∖↑mgmtN)).
@@ -134,8 +134,6 @@ Proof.
     set_solver. }
   { done. }
   iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
-  { (* FIXME solve_ndisj should really handle this... *)
-    assert (↑mgmtN ⊆ ↑lftN) by solve_ndisj. set_solver. }
   rewrite /lft_tok big_sepMS_singleton.
   iDestruct (own_valid_2 with "HA HΛ")
     as %[[s [?%leibniz_equiv ?]]%singleton_included_l _]%auth_both_valid_discrete.
@@ -172,7 +170,7 @@ 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 bbd57d69bacea33e326207680b9373a683a1395d..fcb5f0fc5a4b8a1c5767e630e2e6ffb237cb160c 100644
--- a/theories/lifetime/model/definitions.v
+++ b/theories/lifetime/model/definitions.v
@@ -38,7 +38,7 @@ Definition ilftUR := gmapUR lft (agreeR lft_namesO).
 Definition borUR := gmapUR slice_name (prodR fracR (agreeR bor_stateO)).
 Definition inhUR := gset_disjUR slice_name.
 
-Class lftG Σ := LftG {
+Class lftGS Σ := LftG {
   lft_box :> boxG Σ;
   alft_inG :> inG Σ (authR alftUR);
   alft_name : gname;
@@ -48,9 +48,9 @@ Class lftG Σ := LftG {
   lft_cnt_inG :> inG Σ (authR natUR);
   lft_inh_inG :> inG Σ (authR inhUR);
 }.
-Definition lftG' := lftG.
+Definition lftGS' := lftGS.
 
-Class lftPreG Σ := LftPreG {
+Class lftGpreS Σ := LftGPreS {
   lft_preG_box :> boxG Σ;
   alft_preG_inG :> inG Σ (authR alftUR);
   ilft_preG_inG :> inG Σ (authR ilftUR);
@@ -58,13 +58,13 @@ Class lftPreG Σ := LftPreG {
   lft_preG_cnt_inG :> inG Σ (authR natUR);
   lft_preG_inh_inG :> inG Σ (authR inhUR);
 }.
-Definition lftPreG' := lftPreG.
+Definition lftGpreS' := lftGpreS.
 
 Definition lftΣ : gFunctors :=
   #[ boxΣ; GFunctor (authR alftUR); GFunctor (authR ilftUR);
      GFunctor (authR borUR); GFunctor (authR natUR); GFunctor (authR inhUR) ].
-Instance subG_lftPreG Σ :
-  subG lftΣ Σ → lftPreG Σ.
+Instance subG_lftGpreS Σ :
+  subG lftΣ Σ → lftGpreS Σ.
 Proof. solve_inG. Qed.
 
 Definition bor_filled (s : bor_state) : bool :=
@@ -77,7 +77,7 @@ Definition to_ilftUR : gmap lft lft_names → ilftUR := fmap to_agree.
 Definition to_borUR : gmap slice_name bor_state → borUR := fmap ((1%Qp,.) ∘ to_agree).
 
 Section defs.
-  Context `{!invG Σ, !lftG Σ}.
+  Context `{!invGS Σ, !lftGS Σ}.
 
   Definition lft_tok (q : Qp) (κ : lft) : iProp Σ :=
     ([∗ mset] Λ ∈ κ, own alft_name (◯ {[ Λ := Cinl q ]}))%I.
@@ -221,7 +221,7 @@ Typeclasses Opaque lft_tok lft_dead bor_cnt lft_bor_alive lft_bor_dead
   idx_bor_own idx_bor raw_bor bor.
 
 Section basic_properties.
-Context `{!invG Σ, !lftG Σ}.
+Context `{!invGS Σ, !lftGS Σ}.
 Implicit Types κ : lft.
 
 (* Unfolding lemmas *)
diff --git a/theories/lifetime/model/faking.v b/theories/lifetime/model/faking.v
index 101ca0ee3fc30468c91df1668d0b2a62e4da1e99..94b0f7969ff60d582a0452b03afeefe64d5fa1d3 100644
--- a/theories/lifetime/model/faking.v
+++ b/theories/lifetime/model/faking.v
@@ -5,7 +5,7 @@ From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 
 Section faking.
-Context `{!invG Σ, !lftG Σ}.
+Context `{!invGS Σ, !lftGS Σ}.
 Implicit Types κ : lft.
 
 Lemma ilft_create A I κ :
diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v
index a5c38259f946d4c8fd096cf75ca87ec787246a93..547d293af1e1718b74254a8d80c0ba7faee33801 100644
--- a/theories/lifetime/model/primitive.v
+++ b/theories/lifetime/model/primitive.v
@@ -7,7 +7,7 @@ Set Default Proof Using "Type".
 Import uPred.
 
 Section primitive.
-Context `{!invG Σ, !lftG Σ}.
+Context `{!invGS Σ, !lftGS Σ}.
 Implicit Types κ : lft.
 
 Lemma to_borUR_included (B : gmap slice_name bor_state) i s q :
@@ -18,8 +18,8 @@ Proof.
   by move=> /Some_pair_included [_] /Some_included_total /to_agree_included=>->.
 Qed.
 
-Lemma lft_init `{!lftPreG Σ} E :
-  ↑lftN ⊆ E → ⊢ |={E}=> ∃ _ : lftG Σ, lft_ctx.
+Lemma lft_init `{!lftGpreS Σ} E :
+  ↑lftN ⊆ E → ⊢ |={E}=> ∃ _ : lftGS Σ, lft_ctx.
 Proof.
   iIntros (?). rewrite /lft_ctx.
   iMod (own_alloc (● ∅ : authR alftUR)) as (γa) "Ha"; first by apply auth_auth_valid.
@@ -300,9 +300,18 @@ Proof.
   intros p q. rewrite /idx_bor_own -own_bor_op /own_bor. f_equiv=>?.
   rewrite -auth_frag_op singleton_op -pair_op agree_idemp. done.
 Qed.
+Global Instance frame_lft_tok p κ q1 q2 RES :
+  FrameFractionalHyps p q1.[κ] (λ q, q.[κ])%I RES q1 q2 →
+  Frame p q1.[κ] q2.[κ] RES | 5.
+Proof. apply: frame_fractional. Qed.
+
 Global Instance idx_bor_own_as_fractional i q :
   AsFractional (idx_bor_own q i) (λ q, idx_bor_own q i)%I q.
 Proof. split. done. apply _. Qed.
+Global Instance frame_idx_bor_own p i q1 q2 RES :
+  FrameFractionalHyps p (idx_bor_own q1 i) (λ q, idx_bor_own q i)%I RES q1 q2 →
+  Frame p (idx_bor_own q1 i) (idx_bor_own q2 i) RES | 5.
+Proof. apply: frame_fractional. Qed.
 
 (** Lifetime inclusion *)
 Lemma lft_incl_acc E κ κ' q :
@@ -357,7 +366,8 @@ Proof.
   iIntros "Hκ Hκ'".
   destruct (Qp_lower_bound q q') as (qq & q0 & q'0 & -> & ->).
   iExists qq. rewrite -lft_tok_sep.
-  iDestruct "Hκ" as "[$$]". iDestruct "Hκ'" as "[$$]". auto.
+  iDestruct "Hκ" as "[$ Hκ]". iDestruct "Hκ'" as "[$ Hκ']".
+  iIntros "[Hκ+ Hκ'+]". iSplitL "Hκ Hκ+"; iApply fractional_split; iFrame.
 Qed.
 
 Lemma lft_incl_glb κ κ' κ'' : κ ⊑ κ' -∗ κ ⊑ κ'' -∗ κ ⊑ κ' ⊓ κ''.
@@ -369,7 +379,9 @@ Proof.
     iDestruct (lft_intersect_acc with "Hκ' Hκ''") as (qq) "[Hqq Hclose]".
     iExists qq. iFrame. iIntros "!> Hqq".
     iDestruct ("Hclose" with "Hqq") as "[Hκ' Hκ'']".
-    iMod ("Hclose'" with "Hκ'") as "$". by iApply "Hclose''".
+    iMod ("Hclose'" with "Hκ'") as "?".
+    iMod ("Hclose''" with "Hκ''") as "?". iModIntro.
+    iApply fractional_half. iFrame.
   - rewrite -lft_dead_or. iIntros "[H†|H†]". by iApply "H1†". by iApply "H2†".
 Qed.
 
diff --git a/theories/lifetime/model/reborrow.v b/theories/lifetime/model/reborrow.v
index 721a53a4f786185d85007a095779d376df988412..d8f6d63e5133161475c322a1e66a2767b2cc47da 100644
--- a/theories/lifetime/model/reborrow.v
+++ b/theories/lifetime/model/reborrow.v
@@ -5,7 +5,7 @@ From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 
 Section reborrow.
-Context `{!invG Σ, !lftG Σ}.
+Context `{!invGS Σ, !lftGS Σ}.
 Implicit Types κ : lft.
 
 (* Notice that taking lft_inv for both κ and κ' already implies
@@ -49,7 +49,7 @@ Proof.
     rewrite /to_borUR !fmap_insert. iFrame "Hbox HB●".
     iDestruct (@big_sepM_delete with "HB") as "[_ HB]"; first done.
     rewrite (big_sepM_delete _ (<[_:=_]>_) i); last by rewrite lookup_insert.
-    rewrite -insert_delete delete_insert ?lookup_delete //=. iFrame; auto. }
+    rewrite -insert_delete_insert delete_insert ?lookup_delete //=. iFrame; auto. }
   clear B HB Pb' Pi'.
   rewrite {1}/lft_bor_alive. iDestruct "Hκalive'" as (B) "(Hbox & >HB● & HB)".
   iMod (slice_insert_full _ _ true with "HP Hbox")
@@ -93,7 +93,7 @@ Proof.
     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.
-    rewrite -insert_delete big_sepM_insert ?lookup_delete //=. by iFrame. }
+    rewrite -insert_delete_insert big_sepM_insert ?lookup_delete //=. by iFrame. }
   iModIntro. rewrite -[S n]Nat.add_1_l -nat_op auth_frag_op own_cnt_op.
   by iFrame.
 Qed.
@@ -135,7 +135,7 @@ Proof.
     as (Pb'') "HH"; [solve_ndisj|done|done| | |].
   { rewrite /lft_bor_alive (big_sepM_delete _ B i') //. iDestruct "HB" as "[_ HB]".
     iExists (delete i' B). rewrite -fmap_delete. iFrame.
-    rewrite fmap_delete -insert_delete delete_insert ?lookup_delete //=. }
+    rewrite fmap_delete -insert_delete_insert delete_insert ?lookup_delete //=. }
   { iNext. iApply (lft_vs_cons with "[] Hvs"). iIntros "[??] _ !>". iNext.
     iRewrite "HeqPb'". iFrame. by iApply "HP'". }
   iDestruct "HH" as "([HI Hinvκ] & $ & Halive & Hvs)".
diff --git a/theories/lifetime/na_borrow.v b/theories/lifetime/na_borrow.v
index 81816c747f5f537d9e670735dc01817679787b24..f9b5932e7278fd3a99a2f44c3bc5f7eb44367e26 100644
--- a/theories/lifetime/na_borrow.v
+++ b/theories/lifetime/na_borrow.v
@@ -3,7 +3,7 @@ From iris.base_logic.lib Require Export na_invariants.
 From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 
-Definition na_bor `{!invG Σ, !lftG Σ, !na_invG Σ}
+Definition na_bor `{!invGS Σ, !lftGS Σ, !na_invG Σ}
            (κ : lft) (tid : na_inv_pool_name) (N : namespace) (P : iProp Σ) :=
   (∃ i, &{κ,i}P ∗ na_inv tid N (idx_bor_own 1 i))%I.
 
@@ -11,7 +11,7 @@ Notation "&na{ κ , tid , N }" := (na_bor κ tid N)
     (format "&na{ κ , tid , N }") : bi_scope.
 
 Section na_bor.
-  Context `{!invG Σ, !lftG Σ, !na_invG Σ}
+  Context `{!invGS Σ, !lftGS Σ, !na_invG Σ}
           (tid : na_inv_pool_name) (N : namespace) (P : iProp Σ).
 
   Global Instance na_bor_ne κ n : Proper (dist n ==> dist n) (na_bor κ tid N).
diff --git a/theories/prophecy/prophecy.v b/theories/prophecy/prophecy.v
index 00b9dae545b54fcbd221883349292fa0933416d1..6c4ac9003bd3388fe6bd11915ff78f2e59fc77db 100644
--- a/theories/prophecy/prophecy.v
+++ b/theories/prophecy/prophecy.v
@@ -2,7 +2,7 @@ Import EqNotations.
 From stdpp Require Import strings.
 From iris.algebra Require Import auth cmra functions gmap csum frac agree.
 From iris.bi Require Import fractional.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.base_logic Require Import invariants.
 From lrust.util Require Import basic vector discrete_fun.
 From lrust.prophecy Require Export syn_type.
@@ -201,7 +201,7 @@ Local Definition proph_sim (S: proph_smryUR) (L: proph_log) :=
 Local Notation "S :~ L" := (proph_sim S L) (at level 70, format "S  :~  L").
 
 Section defs.
-Context `{!invG Σ, !prophG Σ}.
+Context `{!invGS Σ, !prophG Σ}.
 
 (** Prophecy Context *)
 Local Definition proph_inv: iProp Σ :=
@@ -231,7 +231,7 @@ Notation "⟨ π , φ ⟩" := (proph_obs (λ π, φ%type%stdpp))
 (** * Iris Lemmas *)
 
 Section proph.
-Context `{!invG Σ, !prophG Σ}.
+Context `{!invGS Σ, !prophG Σ}.
 
 (** Instances *)
 
@@ -245,9 +245,17 @@ Proof.
 Qed.
 Global Instance proph_tok_as_fractional q ξ : AsFractional q:[ξ] (λ q, q:[ξ]%I) q.
 Proof. split; by [|apply _]. Qed.
+Global Instance frame_proph_tok p ξ q1 q2 RES :
+  FrameFractionalHyps p q1:[ξ] (λ q, q:[ξ])%I RES q1 q2 →
+  Frame p q1:[ξ] q2:[ξ] RES | 5.
+Proof. apply: frame_fractional. Qed.
 
 Global Instance proph_toks_as_fractional q ξl : AsFractional q:+[ξl] (λ q, q:+[ξl]%I) q.
 Proof. split; by [|apply _]. Qed.
+Global Instance frame_proph_toks p ξl q1 q2 RES :
+  FrameFractionalHyps p q1:+[ξl] (λ q, q:+[ξl])%I RES q1 q2 →
+  Frame p q1:+[ξl] q2:+[ξl] RES | 5.
+Proof. apply: frame_fractional. Qed.
 
 Global Instance proph_obs_persistent φπ : Persistent .⟨φπ⟩ := _.
 Global Instance proph_obs_timeless φπ : Timeless .⟨φπ⟩ := _.
@@ -272,8 +280,9 @@ Lemma proph_tok_combine ξl ζl q q' :
   q:+[ξl] -∗ q':+[ζl] -∗
     ∃q'', q'':+[ξl ++ ζl] ∗ (q'':+[ξl ++ ζl] -∗ q:+[ξl] ∗ q':+[ζl]).
 Proof.
-  case (Qp_lower_bound q q')=> [q''[?[?[->->]]]]. iIntros "[ξl $][ζl $]".
-  iExists q''. iIntros "{$ξl $ζl}[$$]".
+  case (Qp_lower_bound q q')=> [q''[?[?[->->]]]]. iIntros "[ξl ξl'][ζl ζl']".
+  iExists q''. iFrame "ξl ζl". iIntros "[ξl ζl]".
+  iSplitL "ξl ξl'"; iApply fractional_split; iFrame.
 Qed.
 
 (** Initialization *)
@@ -425,13 +434,13 @@ Global Opaque proph_ctx proph_tok proph_obs.
 
 (** * Prophecy Equalizer *)
 
-Definition proph_eqz `{!invG Σ, !prophG Σ} {A} (uπ vπ: proph A) : iProp Σ :=
+Definition proph_eqz `{!invGS Σ, !prophG Σ} {A} (uπ vπ: proph A) : iProp Σ :=
   ∀E ξl q, ⌜↑prophN ⊆ E ∧ vπ ./ ξl⌝ -∗ q:+[ξl] ={E}=∗ ⟨π, uπ π = vπ π⟩ ∗ q:+[ξl].
 
 Notation "uπ :== vπ" := (proph_eqz uπ vπ) (at level 70, format "uπ  :==  vπ") : bi_scope.
 
 Section proph_eqz.
-Context `{!invG Σ, !prophG Σ}.
+Context `{!invGS Σ, !prophG Σ}.
 
 (** ** Constructing Prophecy Equalizers *)
 
diff --git a/theories/prophecy/syn_type.v b/theories/prophecy/syn_type.v
index d4a75ce784bfac828271e922bede4a06fffbef78..bad469b89064f116b58a2f3ec94fd67788eae1bf 100644
--- a/theories/prophecy/syn_type.v
+++ b/theories/prophecy/syn_type.v
@@ -62,7 +62,7 @@ Proof.
   try (by split; [move=> ->|move=> [=]]);
   by split; [move=> [->->]|move=> [=]].
 Qed.
-Instance syn_type_beq_dec: EqDecision syn_type.
+Global Instance syn_type_beq_dec: EqDecision syn_type.
 Proof.
   refine (λ 𝔄 𝔅, cast_if (decide (syn_type_beq 𝔄 𝔅)));
   by rewrite -syn_type_eq_correct.
diff --git a/theories/typing/array.v b/theories/typing/array.v
index c0b3da4ecfdd5cf0b564d8c15a9b9fdfdb25de4a..9fbe383cc750c1b52e3e488d544f32edb1bfe2c8 100644
--- a/theories/typing/array.v
+++ b/theories/typing/array.v
@@ -156,12 +156,12 @@ Section typing.
   Qed.
 
   Lemma array_plus_prod {𝔄} m n (ty: type 𝔄) E L :
-    eqtype E L [ty;^ m + n] ([ty;^ m] * [ty;^ n]) (vsepat m) (curry vapp).
+    eqtype E L [ty;^ m + n] ([ty;^ m] * [ty;^ n]) (vsepat m) (uncurry vapp).
   Proof.
     apply eqtype_symm, eqtype_unfold; [apply _|]. iIntros (?) "_!>_".
     iSplit; [iPureIntro=>/=; lia|]. iSplit.
     { rewrite/= lft_intersect_list_app. iApply lft_intersect_equiv_idemp. }
-    have Eq: ∀vπ: proph (vec 𝔄 _ * _), vfunsep (curry vapp ∘ vπ) =
+    have Eq: ∀vπ: proph (vec 𝔄 _ * _), vfunsep (uncurry vapp ∘ vπ) =
       vfunsep (fst ∘ vπ) +++ vfunsep (snd ∘ vπ).
     { move=> ?? vπ. have {1}<-: pair ∘ vapply (vfunsep $ fst ∘ vπ) ⊛
       vapply (vfunsep $ snd ∘ vπ) = vπ by rewrite !semi_iso' -surjective_pairing_fun.
@@ -179,7 +179,7 @@ Section typing.
   Qed.
 
   Lemma array_succ_prod {𝔄} n (ty: type 𝔄) E L :
-    eqtype E L [ty;^ S n] (ty * [ty;^ n]) (λ v, (vhd v, vtl v)) (curry (λ x, vcons x)).
+    eqtype E L [ty;^ S n] (ty * [ty;^ n]) (λ v, (vhd v, vtl v)) (uncurry (λ x, vcons x)).
   Proof.
     eapply eqtype_eq.
     - eapply eqtype_trans; [apply (array_plus_prod 1)|].
diff --git a/theories/typing/array_util.v b/theories/typing/array_util.v
index 398bfbdcf389ed0948b223585bec7af0a8767e83..093beb94e059ae5da9c2571416c2a026bf055991 100644
--- a/theories/typing/array_util.v
+++ b/theories/typing/array_util.v
@@ -47,7 +47,7 @@ Section array_util.
   Qed.
 
   Lemma ty_share_big_sepL {𝔄} (ty: type 𝔄) E aπl d κ l tid q :
-    ↑lftN ⊆ E → lft_ctx -∗ κ ⊑ ty.(ty_lft) -∗
+    ↑lftN ⊆ E → lft_ctx -∗ κ ⊑ ty_lft ty -∗
     &{κ} ([∗ list] i ↦ aπ ∈ aπl, (l +ₗ[ty] i) ↦∗: ty.(ty_own) aπ d tid) -∗ q.[κ]
       ={E}=∗ |={E}▷=>^d |={E}=>
         ([∗ list] i ↦ aπ ∈ aπl, ty.(ty_shr) aπ d κ tid (l +ₗ[ty] i)) ∗ q.[κ].
@@ -64,7 +64,7 @@ Section array_util.
   Qed.
 
   Lemma ty_own_proph_big_sepL {𝔄} (ty: type 𝔄) n E (aπl: vec _ n) wll d tid κ q :
-    ↑lftN ⊆ E → lft_ctx -∗ κ ⊑ ty.(ty_lft) -∗
+    ↑lftN ⊆ E → lft_ctx -∗ κ ⊑ ty_lft ty -∗
     ([∗ list] i ↦ aπwl ∈ vzip aπl wll, ty.(ty_own) aπwl.1 d tid aπwl.2) -∗ q.[κ]
       ={E}=∗ |={E}▷=>^d |={E}=> ∃ξl q', ⌜vapply aπl ./ ξl⌝ ∗ q':+[ξl] ∗
         (q':+[ξl] ={E}=∗
@@ -85,7 +85,7 @@ Section array_util.
   Qed.
 
   Lemma ty_own_proph_big_sepL_mt {𝔄} (ty: type 𝔄) n E (aπl: vec _ n) l d tid κ q :
-    ↑lftN ⊆ E → lft_ctx -∗ κ ⊑ ty.(ty_lft) -∗
+    ↑lftN ⊆ E → lft_ctx -∗ κ ⊑ ty_lft ty -∗
     ([∗ list] i ↦ aπ ∈ aπl, (l +ₗ[ty] i) ↦∗: ty.(ty_own) aπ d tid) -∗ q.[κ]
       ={E}=∗ |={E}▷=>^d |={E}=> ∃ξl q', ⌜vapply aπl ./ ξl⌝ ∗ q':+[ξl] ∗
         (q':+[ξl] ={E}=∗
@@ -100,7 +100,7 @@ Section array_util.
   Qed.
 
   Lemma ty_shr_proph_big_sepL {𝔄} (ty: type 𝔄) n E (aπl: vec _ n) d κ tid l κ' q :
-    ↑lftN ⊆ E → lft_ctx -∗ κ' ⊑ κ -∗ κ' ⊑ ty.(ty_lft) -∗
+    ↑lftN ⊆ E → lft_ctx -∗ κ' ⊑ κ -∗ κ' ⊑ ty_lft ty -∗
     ([∗ list] i ↦ aπ ∈ aπl, ty.(ty_shr) aπ d κ tid (l +ₗ[ty] i)) -∗ q.[κ']
       ={E}▷=∗ |={E}▷=>^d |={E}=> ∃ξl q', ⌜vapply aπl ./ ξl⌝ ∗ q':+[ξl] ∗
         (q':+[ξl] ={E}=∗ q.[κ']).
diff --git a/theories/typing/cont_context.v b/theories/typing/cont_context.v
index fac1429566a1a76e5fc58b590a95a7060ddbcacf..a431a62d84fe29281ba3c588d39abafe9c0572ce 100644
--- a/theories/typing/cont_context.v
+++ b/theories/typing/cont_context.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From lrust.lang Require Import notation.
 From lrust.typing Require Import type lft_contexts type_context.
 Set Default Proof Using "Type".
diff --git a/theories/typing/examples/get_x.v b/theories/typing/examples/get_x.v
index 94e8665ed842e7f1dabc36781c92c0bbc0c58279..c8348721eee40cda8d3bee65fc072ca06970cf13 100644
--- a/theories/typing/examples/get_x.v
+++ b/theories/typing/examples/get_x.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
diff --git a/theories/typing/examples/inc_vec.v b/theories/typing/examples/inc_vec.v
index 5f806925cc2260ffbbde15990dc1d6154c957220..3fb3fb67ac6a08a7931e6608a50f1d7afac8fbeb 100644
--- a/theories/typing/examples/inc_vec.v
+++ b/theories/typing/examples/inc_vec.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From lrust.typing Require Export type.
 From lrust.typing Require Import typing.
 From lrust.typing.lib.vec Require Import vec vec_slice.
diff --git a/theories/typing/examples/init_prod.v b/theories/typing/examples/init_prod.v
index 53268f2c4c590a3acedbbb1f2dceb0debd78b07a..b4a50aaac9b0832ec09b3797a9dbf5c19f39b38c 100644
--- a/theories/typing/examples/init_prod.v
+++ b/theories/typing/examples/init_prod.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
diff --git a/theories/typing/examples/lazy_lft.v b/theories/typing/examples/lazy_lft.v
index f0b562f28e014de22a1849095f63f577f0f7b815..4a1776005a171b7afc5eb9573d90143b1c913dd3 100644
--- a/theories/typing/examples/lazy_lft.v
+++ b/theories/typing/examples/lazy_lft.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
diff --git a/theories/typing/examples/nonlexical.v b/theories/typing/examples/nonlexical.v
index 9759813c5d79860c1740b3e99a6ea12a6830b395..a543759aca3b595b4a65253013fd42067a7286b9 100644
--- a/theories/typing/examples/nonlexical.v
+++ b/theories/typing/examples/nonlexical.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From lrust.typing Require Import typing lib.option.
 
 (* Typing "problem case #3" from:
diff --git a/theories/typing/examples/projection_toggle.v b/theories/typing/examples/projection_toggle.v
index 80c2cf7d931ced47fc695629257331ca0cd74be4..a3b72ae0eb656ef6e53ad0fc2f3b87e319f50104 100644
--- a/theories/typing/examples/projection_toggle.v
+++ b/theories/typing/examples/projection_toggle.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From lrust.typing Require Export type.
 From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
diff --git a/theories/typing/examples/rebor.v b/theories/typing/examples/rebor.v
index f8a7eb7a4ddcc22ab7bba4317855dbed5781a531..e23c30c4e0a3229c9bd696bd8f9f321f95e991fe 100644
--- a/theories/typing/examples/rebor.v
+++ b/theories/typing/examples/rebor.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
diff --git a/theories/typing/examples/unbox.v b/theories/typing/examples/unbox.v
index 82e11937d08afae39c9e4d166334374449625e7b..9b46ac8b5f113ba30ff2c6509df786de6264a3e8 100644
--- a/theories/typing/examples/unbox.v
+++ b/theories/typing/examples/unbox.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
diff --git a/theories/typing/fixpoint.v b/theories/typing/fixpoint.v
index b94ed7cf6e90d13c678882fc151bd4dc7db9242e..db14e95c217e498b842bb9c1ac3f9cc5313dda22 100644
--- a/theories/typing/fixpoint.v
+++ b/theories/typing/fixpoint.v
@@ -13,9 +13,9 @@ Section S.
 
   Definition Tn n := Nat.iter (S n) T base.
 
-  Lemma Tn_ty_lft_const n n' : ⊢ (Tn n).(ty_lft) ≡ₗ (Tn n').(ty_lft).
+  Lemma Tn_ty_lft_const n n' : ⊢ ty_lft (Tn n) ≡ₗ ty_lft (Tn n').
   Proof using HT.
-    have Eq: ∀n, ⊢ (Tn n).(ty_lft) ≡ₗ (Tn 0).(ty_lft); last first.
+    have Eq: ∀n, ⊢ ty_lft (Tn n) ≡ₗ ty_lft (Tn 0); last first.
     { iApply lft_equiv_trans; [|iApply lft_equiv_sym]; iApply Eq. }
     clear n n'=> n. case type_contractive_type_lft_morphism=> [> Hα ?|> Hα ?]; last first.
     { iApply lft_equiv_trans; [iApply Hα|]. iApply lft_equiv_sym. iApply Hα. }
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 7bab016a316909d33de475580249d585aa9a6da2..cbabd1f0816fe6dfc8a628ceeaec32c9651d315c 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -383,7 +383,7 @@ Section typing.
     move: Cl. rewrite Into. iIntros (? Body ?????) "_ _ _ _ _ $$ _ Obs".
     iMod persistent_time_receipt_0 as "#⧖". iApply wp_value. iExists -[const tr].
     iFrame "Obs". iSplit; [|done]. iLöb as "IH". iExists _, 0%nat.
-    iSplit; [by rewrite/= decide_left|]. iFrame "⧖". iExists tr.
+    iSplit; [by rewrite/= decide_True_pi|]. iFrame "⧖". iExists tr.
     iSplit; [done|]. iExists fb, "return", bl', e, _. iSplit; [done|].
     iIntros "!>!> *%%% LFT TIME PROPH UNIQ Efp Na L C T ?".
     iApply (Body _ _ (RecV _ _ _) $! _ (_-::_) with
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index 6e1ef5b3b6ff5a305bed1d8379ed2fa887e79c24..685830cdeb9db4c002d3e94ad099a0523c1caa40 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -24,12 +24,12 @@ Notation llctx := (list llctx_elt).
 Notation "κ ⊑ₗ κl" := (@pair lft (list lft) κ κl) (at level 55).
 
 (* External lifetime context. *)
-Definition elctx_elt_interp `{!invG Σ, !lftG Σ} (x : elctx_elt) : iProp Σ :=
+Definition elctx_elt_interp `{!invGS Σ, !lftGS Σ} (x : elctx_elt) : iProp Σ :=
   (x.1 ⊑ x.2)%I.
 Notation elctx_interp := (big_sepL (λ _, elctx_elt_interp)).
 
 Section lft_contexts.
-  Context `{!invG Σ, !lftG Σ}.
+  Context `{!invGS Σ, !lftGS Σ}.
   Implicit Type (κ: lft).
 
   Global Instance elctx_interp_permut :
@@ -56,7 +56,7 @@ Section lft_contexts.
       iDestruct "Hq" as (κ0) "(% & Hq & #?)".
       iDestruct "Hq'" as (κ0') "(% & Hq' & #?)". simpl in *.
       rewrite (inj ((lft_intersect_list κs) ⊓.) κ0' κ0); last congruence.
-      iExists κ0. by iFrame "∗%".
+      iExists κ0. iFrame "∗%". done.
   Qed.
 
   Definition llctx_interp (L : llctx) (q : Qp) : iProp Σ :=
@@ -68,6 +68,11 @@ Section lft_contexts.
   Global Instance llctx_interp_as_fractional L q :
     AsFractional (llctx_interp L q) (llctx_interp L) q.
   Proof. split. done. apply _. Qed.
+  Global Instance frame_llctx_interp p L q1 q2 RES :
+    FrameFractionalHyps p (llctx_interp L q1) (llctx_interp L) RES q1 q2 →
+    Frame p (llctx_interp L q1) (llctx_interp L q2) RES | 5.
+  Proof. apply: frame_fractional. Qed.
+
   Global Instance llctx_interp_permut :
     Proper ((≡ₚ) ==> eq ==> (⊣⊢)) llctx_interp.
   Proof. intros ????? ->. by apply big_opL_permutation. Qed.
@@ -347,7 +352,7 @@ Arguments elctx_sat {_ _ _} _ _ _.
 Arguments lctx_lft_incl_incl {_ _ _ _ _} _ _.
 Arguments lctx_lft_alive_tok {_ _ _ _ _} _ _ _.
 
-Lemma elctx_sat_submseteq `{!invG Σ, !lftG Σ} E E' L :
+Lemma elctx_sat_submseteq `{!invGS Σ, !lftGS Σ} E E' L :
   E' ⊆+ E → elctx_sat E L E'.
 Proof. iIntros (HE' ?) "_ !> H". by iApply big_sepL_submseteq. Qed.
 
diff --git a/theories/typing/lib/arc.v b/theories/typing/lib/arc.v
index b89618e35022ff9d7c084f511849f1b91e46df4c..b6c1510d0fe3b877b4d258618c5624f47dd0602c 100644
--- a/theories/typing/lib/arc.v
+++ b/theories/typing/lib/arc.v
@@ -25,7 +25,7 @@ Section arc.
      (* We use this disjunction, and not simply [ty_shr] here, *)
      (*    because [weak_new] cannot prove ty_shr, even for a dead *)
      (*    lifetime. *)
-     (ty.(ty_shr) (ν ⊓ ty.(ty_lft)) tid (l +ₗ 2) ∨ [†ν]) ∗
+     (ty.(ty_shr) (ν ⊓ ty_lft ty) tid (l +ₗ 2) ∨ [†ν]) ∗
      □ (1.[ν] ={↑lftN ∪ ↑lft_userN ∪ ↑arc_endN}[↑lft_userN]▷=∗
           [†ν] ∗ ▷ (l +ₗ 2) ↦∗: ty.(ty_own) tid ∗ † l…(2 + ty.(ty_size))))%I.
 
@@ -63,8 +63,8 @@ Section arc.
     (∃ γ ν q, arc_persist tid ν γ l ty ∗ arc_tok γ q ∗ q.[ν])%I.
   Lemma arc_own_share E l ty tid q :
     ↑lftN ⊆ E →
-    lft_ctx -∗ (q).[ty.(ty_lft)] -∗ full_arc_own l ty tid
-    ={E}=∗ (q).[ty.(ty_lft)] ∗ shared_arc_own l ty tid.
+    lft_ctx -∗ (q).[ty_lft ty] -∗ full_arc_own l ty tid
+    ={E}=∗ (q).[ty_lft ty] ∗ shared_arc_own l ty tid.
   Proof.
     iIntros (?) "#LFT Htok (Hl1 & Hl2 & H† & Hown)".
     iMod (lft_create with "LFT") as (ν) "[Hν #Hν†]"=>//.
@@ -806,7 +806,7 @@ Section arc.
     iAssert (shared_arc_own rc' ty tid ∗ llctx_interp [ϝ ⊑ₗ []] 1)%I
       with "[>Hrc' HL]" as "[Hrc' HL]".
     { iDestruct "Hrc'" as "[?|$]"; last done.
-      iMod (lctx_lft_alive_tok ty.(ty_lft) with "HE HL")
+      iMod (lctx_lft_alive_tok ty_lft ty with "HE HL")
         as (?) "(Htok & HL & Hclose)"; [done| |].
       { change (ty_outlives_E (arc ty)) with (ty_outlives_E ty).
         eapply (lctx_lft_alive_incl _ _ ϝ); first solve_typing.
@@ -921,7 +921,7 @@ Section arc.
     iAssert (shared_arc_own rc' ty tid ∗ llctx_interp [ϝ ⊑ₗ []] 1)%I
       with "[>Hrc' HL]" as "[Hrc' HL]".
     { iDestruct "Hrc'" as "[?|$]"; last done.
-      iMod (lctx_lft_alive_tok ty.(ty_lft) with "HE HL")
+      iMod (lctx_lft_alive_tok ty_lft ty with "HE HL")
         as (?) "(Htok & HL & Hclose)"; [done| |].
       { change (ty_outlives_E (arc ty)) with (ty_outlives_E ty).
         eapply (lctx_lft_alive_incl _ _ ϝ); first solve_typing.
diff --git a/theories/typing/lib/diverging_static.v b/theories/typing/lib/diverging_static.v
index 1d09e83c8d8e8a25a33571ba6f6c3ad99ff825fb..ccfd10c9027e5df28445dde50cdcfd9242053465 100644
--- a/theories/typing/lib/diverging_static.v
+++ b/theories/typing/lib/diverging_static.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From lrust.typing Require Export type.
 From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
diff --git a/theories/typing/lib/fake_shared.v b/theories/typing/lib/fake_shared.v
index ebaa3764c94a061e1b37cba27c222b78dd370d17..55c03115fa49940cb0082f1d01c2cf66b0f60cde 100644
--- a/theories/typing/lib/fake_shared.v
+++ b/theories/typing/lib/fake_shared.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
diff --git a/theories/typing/lib/join.v b/theories/typing/lib/join.v
index 8516d2db84b2cd93c18b791dfecbb32e970b3b76..321c75a96d14326f8d6e6c0cda4bc1dda8f6301f 100644
--- a/theories/typing/lib/join.v
+++ b/theories/typing/lib/join.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From lrust.lang Require Import spawn.
 From lrust.typing Require Export type.
 From lrust.typing Require Import typing.
diff --git a/theories/typing/lib/mutex/mutex.v b/theories/typing/lib/mutex/mutex.v
index 146ffcdda17ddc189606c78490630fd5f7fee7fb..bbfc0d5bfdbd2c90bbf9d0fee03f5f645dbcac8f 100644
--- a/theories/typing/lib/mutex/mutex.v
+++ b/theories/typing/lib/mutex/mutex.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.algebra Require Import auth csum frac agree.
 From lrust.lang.lib Require Import memcpy lock.
 From lrust.lifetime Require Import na_borrow.
@@ -63,7 +63,7 @@ Section mutex.
       ty_own Φπ _ tid vl := ∃Φ (b: bool) vl' (vπ: proph 𝔄) d,
         ⌜vl = #b :: vl' ∧ Φπ = const Φ⌝ ∗
         ⟨π, Φ (vπ π)⟩ ∗ ⧖(S d) ∗ ty.(ty_own) vπ d tid vl';
-      ty_shr Φπ _ κ tid l := ∃Φ κ', ⌜Φπ = const Φ⌝ ∗ κ ⊑ κ' ∗ κ' ⊑ ty.(ty_lft) ∗
+      ty_shr Φπ _ κ tid l := ∃Φ κ', ⌜Φπ = const Φ⌝ ∗ κ ⊑ κ' ∗ κ' ⊑ ty_lft ty ∗
         &at{κ, mutexN} (lock_proto l (mutex_body ty Φ κ' l tid));
     |}%I.
   Next Obligation.
diff --git a/theories/typing/lib/mutex/mutexguard.v b/theories/typing/lib/mutex/mutexguard.v
index 3f2254364752012143a0d7963c3d1430f0792924..4903e427c8253f8118c1a7b0a7e0bd1d5461f332 100644
--- a/theories/typing/lib/mutex/mutexguard.v
+++ b/theories/typing/lib/mutex/mutexguard.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.algebra Require Import auth csum frac agree.
 From lrust.lang.lib Require Import memcpy lock.
 From lrust.lifetime Require Import na_borrow.
@@ -46,11 +46,11 @@ Section mutexguard.
     ty_size := 1;  ty_lfts := κ :: ty.(ty_lfts);  ty_E := ty.(ty_E) ++ ty_outlives_E ty κ;
     (* One logical step is required for [ty_share] *)
     ty_own Φπ d tid vl := ⌜d > 0⌝ ∗ [loc[l] := vl] ∃Φ κ',
-      ⌜Φπ = const Φ⌝ ∗ κ ⊑ κ' ∗ κ' ⊑ ty.(ty_lft) ∗
+      ⌜Φπ = const Φ⌝ ∗ κ ⊑ κ' ∗ κ' ⊑ ty_lft ty ∗
       &at{κ, mutexN} (lock_proto l (mutex_body ty Φ κ' l tid)) ∗
       mutex_body ty Φ κ' l tid;
     ty_shr Φπ _ κ' tid l := ∃Φ (l': loc) κᵢ (vπ: proph 𝔄) d,
-      ⌜Φπ = const Φ⌝ ∗ κ' ⊑ κᵢ ∗ κᵢ ⊑ ty.(ty_lft) ∗
+      ⌜Φπ = const Φ⌝ ∗ κ' ⊑ κᵢ ∗ κᵢ ⊑ ty_lft ty ∗
       &frac{κ'}(λ q', l ↦{q'} #l') ∗ ⟨π, Φ (vπ π)⟩ ∗ ⧖(S d) ∗
       □ ∀E q, ⌜↑lftN ∪ ↑shrN ⊆ E⌝ -∗ q.[κᵢ]
         ={E,E∖↑shrN}=∗ |={E∖↑shrN}▷=>^(S d) |={E∖↑shrN,E}=>
@@ -87,7 +87,7 @@ Section mutexguard.
     iMod (inv_alloc shrN _ (_ ∨ ty.(ty_shr) _ _ _ _ _)%I with "[Bor]") as "#inv".
     { iLeft. iNext. iExact "Bor". }
     iModIntro. iFrame "κ'". iExists _, _, κᵢ, _, _. iSplit; [done|].
-    iFrame "Bor↦ Obs ⧖ κ'⊑κᵢ". iAssert (κᵢ ⊑ ty.(ty_lft))%I as "#?".
+    iFrame "Bor↦ Obs ⧖ κ'⊑κᵢ". iAssert (κᵢ ⊑ ty_lft ty)%I as "#?".
     { iApply lft_incl_trans; [iApply lft_intersect_incl_l|done]. }
     iSplit; [done|]. iIntros "!>" (???) "κᵢ".
     iInv shrN as "[Bor|#ty]" "Close"; iIntros "/=!>!>!>"; last first.
@@ -131,7 +131,8 @@ Section mutexguard.
   Global Instance mutexguard_send {𝔄} κ (ty: type 𝔄) :
     Send ty → Send (mutexguard κ ty).
   Proof.
-    move=> ?>/=. rewrite /mutex_body. do 21 f_equiv; [|done]. by do 2 f_equiv.
+    move=> ?>/=. rewrite /mutex_body. do 21 (f_equiv || move=>?); [|done].
+    by do 2 f_equiv.
   Qed.
 
   (* In order to prove [mutexguard_resolve] with a non-trivial postcondition,
diff --git a/theories/typing/lib/panic.v b/theories/typing/lib/panic.v
index 972529d099611fc15df4e67f0e181d69809bc8a8..d54072769c33c9eb77ea8a999697d94afb386adf 100644
--- a/theories/typing/lib/panic.v
+++ b/theories/typing/lib/panic.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index ccd2608e5118e26b21e8814327ce0963005bc174..989138bd9b80927d822783a15d02f2b135b61c97 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.algebra Require Import auth csum frac agree excl numbers.
 From lrust.lang.lib Require Import memcpy.
 From lrust.lifetime Require Import na_borrow.
@@ -77,7 +77,7 @@ Section rc.
               (* We use this disjunction, and not simply [ty_shr] here,
                  because [weak_new] cannot prove ty_shr, even for a dead
                  lifetime. *)
-              (ty.(ty_shr) (ν ⊓ ty.(ty_lft)) tid (l +ₗ 2) ∨ [†ν]) ∗
+              (ty.(ty_shr) (ν ⊓ ty_lft ty) tid (l +ₗ 2) ∨ [†ν]) ∗
               □ (1.[ν] ={↑lftN ∪ ↑lft_userN}[↑lft_userN]▷=∗ [†ν]))%I.
 
   Global Instance rc_persist_persistent tid ν γ l ty : Persistent (rc_persist tid ν γ l ty).
diff --git a/theories/typing/lib/rc/weak.v b/theories/typing/lib/rc/weak.v
index 77e402148025804a4e9d7471ace05f21af3ea732..b800f535eea83c2f482ad06d6a50557aaa9fda76 100644
--- a/theories/typing/lib/rc/weak.v
+++ b/theories/typing/lib/rc/weak.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.algebra Require Import auth csum frac agree numbers.
 From lrust.lang.lib Require Import memcpy.
 From lrust.lifetime Require Import na_borrow.
diff --git a/theories/typing/lib/refcell/ref.v b/theories/typing/lib/refcell/ref.v
index ae10f43d67bb7abce0f4df39faf6dedcc164b796..220b915c90d68b0e930c8287ff73bf1dee3ab0f0 100644
--- a/theories/typing/lib/refcell/ref.v
+++ b/theories/typing/lib/refcell/ref.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.algebra Require Import auth csum frac agree.
 From iris.bi Require Import fractional.
 From lrust.lifetime Require Import na_borrow.
diff --git a/theories/typing/lib/refcell/ref_code.v b/theories/typing/lib/refcell/ref_code.v
index 1af1e8dce21eaf2f73e499390d46faf0c288eba4..befa9dbca41c5246de78d2d8682102b1161e13d5 100644
--- a/theories/typing/lib/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.algebra Require Import auth csum frac agree numbers.
 From iris.bi Require Import fractional.
 From lrust.lifetime Require Import lifetime na_borrow.
diff --git a/theories/typing/lib/refcell/refcell.v b/theories/typing/lib/refcell/refcell.v
index e7f5e6575462143e2c23aba869af78980aa11d03..5573e83fc912b20cbb84727e81c6e0e5fb37655d 100644
--- a/theories/typing/lib/refcell/refcell.v
+++ b/theories/typing/lib/refcell/refcell.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.algebra Require Import auth csum frac agree numbers.
 From iris.bi Require Import fractional.
 From lrust.lifetime Require Import na_borrow.
@@ -101,7 +101,7 @@ Section refcell.
          | _ => False
          end%I;
        ty_shr κ tid l :=
-         (∃ α γ, κ ⊑ α ∗ α ⊑ ty.(ty_lft) ∗
+         (∃ α γ, κ ⊑ α ∗ α ⊑ ty_lft ty ∗
                  &na{α, tid, refcell_invN}(refcell_inv tid l γ α ty))%I |}.
   Next Obligation.
     iIntros (??[|[[]|]]); try iIntros "[]". rewrite ty_size_eq /=. by iIntros (->).
diff --git a/theories/typing/lib/refcell/refcell_code.v b/theories/typing/lib/refcell/refcell_code.v
index af7face2cd680c0eb58380543d595aa69e030bba..d5070402446e389d8bb7a01ca16ada1a479fcc3c 100644
--- a/theories/typing/lib/refcell/refcell_code.v
+++ b/theories/typing/lib/refcell/refcell_code.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.algebra Require Import auth csum frac agree.
 From iris.bi Require Import fractional.
 From lrust.lang.lib Require Import memcpy.
diff --git a/theories/typing/lib/refcell/refmut.v b/theories/typing/lib/refcell/refmut.v
index 7332c953febc457fe0ebe47c79da5c02477bbba5..8e634a2e8eafffdb997b8e9b15fc13fb3502a36f 100644
--- a/theories/typing/lib/refcell/refmut.v
+++ b/theories/typing/lib/refcell/refmut.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.algebra Require Import auth csum frac agree.
 From iris.bi Require Import fractional.
 From lrust.lifetime Require Import na_borrow.
@@ -27,7 +27,7 @@ Section refmut.
          match vl return _ with
          | [ #(LitLoc lv);  #(LitLoc lrc) ] =>
            ∃ ν q γ β ty', &{α ⊓ ν}(lv ↦∗: ty.(ty_own) tid) ∗
-             α ⊑ β ∗ α ⊓ ν ⊑ ty.(ty_lft) ∗
+             α ⊑ β ∗ α ⊓ ν ⊑ ty_lft ty ∗
              &na{β, tid, refcell_invN}(refcell_inv tid lrc γ β ty') ∗
              q.[ν] ∗ own γ (◯ writing_stR q ν)
          | _ => False
diff --git a/theories/typing/lib/refcell/refmut_code.v b/theories/typing/lib/refcell/refmut_code.v
index 4ba8143286ac0058eeb08d285543768be33efcb1..b23d8fa6ce06a70ce3a2832e85db96a277ee9428 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.algebra Require Import auth csum frac agree numbers.
 From iris.bi Require Import fractional.
 From lrust.lifetime Require Import na_borrow.
diff --git a/theories/typing/lib/rwlock/rwlock.v b/theories/typing/lib/rwlock/rwlock.v
index 961cd95f457aea2ad8d04da3ec1591cd54f8336a..736d26ede4534c2f74fe1e6a806da704364e1e5a 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.algebra Require Import auth csum frac agree excl numbers.
 From iris.bi Require Import fractional.
 From lrust.lifetime Require Import at_borrow.
@@ -108,7 +108,7 @@ Section rwlock.
          | _ => False
          end%I;
        ty_shr κ tid l :=
-         (∃ α γ, κ ⊑ α ∗ α ⊑ ty.(ty_lft) ∗
+         (∃ α γ, κ ⊑ α ∗ α ⊑ ty_lft ty ∗
                  &at{α,rwlockN}(rwlock_inv tid tid l γ α ty))%I |}.
   Next Obligation.
     iIntros (??[|[[]|]]); try iIntros "[]". rewrite ty_size_eq.
diff --git a/theories/typing/lib/rwlock/rwlock_code.v b/theories/typing/lib/rwlock/rwlock_code.v
index 3b21c2d843d037038af996e71c5e3ace9e52726e..b8ab832b378f3e9ebb2f7bea1febb85fa19baefb 100644
--- a/theories/typing/lib/rwlock/rwlock_code.v
+++ b/theories/typing/lib/rwlock/rwlock_code.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.algebra Require Import auth csum frac agree.
 From iris.bi Require Import fractional.
 From lrust.lang.lib Require Import memcpy.
diff --git a/theories/typing/lib/rwlock/rwlockreadguard.v b/theories/typing/lib/rwlock/rwlockreadguard.v
index 4d1621905ece8ed6e07750d2c4d755ab5afb732a..83b652e18175f4975532f1e1aba95654ddbcd572 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.algebra Require Import auth csum frac agree.
 From iris.bi Require Import fractional.
 From lrust.lifetime Require Import na_borrow.
diff --git a/theories/typing/lib/rwlock/rwlockreadguard_code.v b/theories/typing/lib/rwlock/rwlockreadguard_code.v
index 6bfda63d6fafcc0dcbbc8c6f4e89b36b849c6f29..acd7ae81afd514b247b14a8fad07f126f75fa4de 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard_code.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.algebra Require Import auth csum frac agree numbers.
 From iris.bi Require Import fractional.
 From lrust.lifetime Require Import lifetime na_borrow.
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard.v b/theories/typing/lib/rwlock/rwlockwriteguard.v
index 7c96791a5394a00c1d84cac32a57fd81d44d9289..69620a054e7ed09fa33b360eed0fb41f6102ef3a 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.algebra Require Import auth csum frac agree.
 From iris.bi Require Import fractional.
 From lrust.lifetime Require Import na_borrow.
@@ -23,7 +23,7 @@ Section rwlockwriteguard.
          match vl return _ with
          | [ #(LitLoc l) ] =>
            ∃ γ β tid_shr, &{β}((l +ₗ 1) ↦∗: ty.(ty_own) tid) ∗
-             α ⊑ β ∗ β ⊑ ty.(ty_lft) ∗
+             α ⊑ β ∗ β ⊑ ty_lft ty ∗
              &at{β,rwlockN}(rwlock_inv tid tid_shr l γ β ty) ∗
              own γ (◯ writing_st)
          | _ => False
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard_code.v b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
index 797ad601117d6474890d734c9e640b1c252c841c..9539be53fc34b744b893b94089041fd239eba020 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.algebra Require Import auth csum frac agree.
 From iris.bi Require Import fractional.
 From lrust.lifetime Require Import na_borrow.
diff --git a/theories/typing/lib/slice/slice.v b/theories/typing/lib/slice/slice.v
index 3cb66a63aa70364b761749491a916b2c08192dc0..f8b91edf7233f93c128afb07ea48b78bf909f3cd 100644
--- a/theories/typing/lib/slice/slice.v
+++ b/theories/typing/lib/slice/slice.v
@@ -82,7 +82,7 @@ Section slice.
   (* Rust's &'a mut [T] *)
   Program Definition uniq_slice {𝔄} (κ: lft) (ty: type 𝔄) : type (listₛ (𝔄 * 𝔄)) := {|
     ty_size := 2;  ty_lfts := κ :: ty.(ty_lfts);  ty_E := ty.(ty_E) ++ ty_outlives_E ty κ;
-    ty_own vπ d tid vl := κ ⊑ ty.(ty_lft) ∗
+    ty_own vπ d tid vl := κ ⊑ ty_lft ty ∗
       ∃(l: loc) (n d': nat) (aπξil: vec (proph 𝔄 * positive) n),
         let aaπl := vmap
           (λ aπξi π, (aπξi.1 π, π (PrVar (𝔄 ↾ prval_to_inh aπξi.1) aπξi.2): 𝔄)) aπξil in
@@ -122,7 +122,8 @@ Section slice.
     iMod (bor_fracture (λ q, q:+[_])%I with "LFT Borξl") as "Borξl"; [done|].
     iModIntro. case d as [|]; [lia|]. iExists _, _, _, _. iFrame "Bor↦ Borξl".
     iSplit; last first.
-    { iClear "#". iNext. iStopProof. do 3 f_equiv. iApply ty_shr_depth_mono. lia. }
+    { iClear "#". iNext. iStopProof. do 3 f_equiv; [|done].
+      iApply ty_shr_depth_mono. lia. }
     iPureIntro. split.
     - fun_ext=>/= ?. by elim aπξil; [done|]=>/= ???->.
     - rewrite /ξl. elim aπξil; [done|]=>/= ????.
diff --git a/theories/typing/lib/slice/slice_basic.v b/theories/typing/lib/slice/slice_basic.v
index 9574c97b90dc31413d7ee99eca12805b2942149a..6aec95782ba0a8e487f195e98ff7416fb67f31db 100644
--- a/theories/typing/lib/slice/slice_basic.v
+++ b/theories/typing/lib/slice/slice_basic.v
@@ -19,7 +19,7 @@ Section slice_basic.
   Qed.
 
   Global Instance shr_slice_send {𝔄} κ (ty: type 𝔄) : Sync ty → Send (shr_slice κ ty).
-  Proof. move=> >/=. by do 12 f_equiv. Qed.
+  Proof. move=> >/=. by do 12 (f_equiv || move=>?). Qed.
 
   Lemma shr_slice_resolve {𝔄} κ (ty: type 𝔄) E L : resolve E L (shr_slice κ ty) (const True).
   Proof. apply resolve_just. Qed.
@@ -76,7 +76,7 @@ Section slice_basic.
   Proof. move=> >/=. rewrite /uniq_body. by do 24 f_equiv. Qed.
 
   Global Instance uniq_slice_sync {𝔄} κ (ty: type 𝔄) : Sync ty → Sync (uniq_slice κ ty).
-  Proof. move=> >/=. by do 17 f_equiv. Qed.
+  Proof. move=> >/=. by do 17 (f_equiv || move=>?). Qed.
 
   Lemma uniq_slice_resolve {𝔄} κ (ty: type 𝔄) E L :
     lctx_lft_alive E L κ →
diff --git a/theories/typing/lib/spawn.v b/theories/typing/lib/spawn.v
index 56e6ad5a41ee51bffc7b457450dbe04a942152cb..54f4b4f58a3fd970d1c13c5eb629c295d7073aaa 100644
--- a/theories/typing/lib/spawn.v
+++ b/theories/typing/lib/spawn.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From lrust.lang Require Import spawn.
 From lrust.typing Require Export type.
 From lrust.typing Require Import typing.
diff --git a/theories/typing/lib/swap.v b/theories/typing/lib/swap.v
index 253fc315ed963e279ad1f9f3099e7ce8e60cea21..0ab8ef55b2973799dc489383d4e8a66ae39ac164 100644
--- a/theories/typing/lib/swap.v
+++ b/theories/typing/lib/swap.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From lrust.lang.lib Require Import swap.
 From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
diff --git a/theories/typing/lib/take_mut.v b/theories/typing/lib/take_mut.v
index c5af236ffb4304d2ad18dc9af99d7286c1fe0df3..0b71a85d5f74f1862366972005b828bbeb23332f 100644
--- a/theories/typing/lib/take_mut.v
+++ b/theories/typing/lib/take_mut.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From lrust.lang.lib Require Import memcpy.
 From lrust.lifetime Require Import na_borrow.
 From lrust.typing Require Export type.
diff --git a/theories/typing/lib/vec/vec_basic.v b/theories/typing/lib/vec/vec_basic.v
index da20c4f287fea37d396f345549cbb8085ba0d855..af9dd03d5a6fee623324ec05bd5c865ff6254ec0 100644
--- a/theories/typing/lib/vec/vec_basic.v
+++ b/theories/typing/lib/vec/vec_basic.v
@@ -17,10 +17,10 @@ Section vec_basic.
   Qed.
 
   Global Instance vec_send {𝔄} (ty: type 𝔄) : Send ty → Send (vec_ty ty).
-  Proof. move=> ?>/=. by do 19 f_equiv. Qed.
+  Proof. move=> ?>/=. by do 19 (f_equiv || move=>?). Qed.
 
   Global Instance vec_sync {𝔄} (ty: type 𝔄) : Sync ty → Sync (vec_ty ty).
-  Proof. move=> ?>/=. by do 16 f_equiv. Qed.
+  Proof. move=> ?>/=. by do 16 (f_equiv || move=>?). Qed.
 
   Lemma vec_resolve {𝔄} (ty: type 𝔄) Φ E L :
     resolve E L ty Φ → resolve E L (vec_ty ty) (lforall Φ).
diff --git a/theories/typing/own.v b/theories/typing/own.v
index e42de1a4aa9f2de5ec3ccdd143b08e1463f43bf0..d06e2d1b668eb33b52e460e8b8ab2a64ea7cb24e 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -36,7 +36,7 @@ Section own.
     - by rewrite left_id shift_loc_0.
     - by rewrite right_id Nat.add_0_r.
     - iSplit; by [iIntros "[??]"|iIntros].
-    - rewrite heap_freeable_op_eq. f_equiv.
+    - rewrite heap_freeable_op_eq. f_equiv; [|done].
       by rewrite -Qp_div_add_distr pos_to_Qp_add -Nat2Pos.inj_add.
   Qed.
 
@@ -108,10 +108,10 @@ Section own.
   Qed.
 
   Global Instance own_send {𝔄} n (ty: type 𝔄) : Send ty → Send (own_ptr n ty).
-  Proof. move=> >/=. by do 9 f_equiv. Qed.
+  Proof. move=> >/=. by do 9 (f_equiv || move=>?). Qed.
 
   Global Instance own_sync {𝔄} n (ty: type 𝔄) : Sync ty → Sync (own_ptr n ty).
-  Proof. move=> >/=. by do 6 f_equiv. Qed.
+  Proof. move=> >/=. by do 6 (f_equiv || move=>?). Qed.
 
   Global Instance own_just_loc {𝔄} n (ty: type 𝔄) : JustLoc (own_ptr n ty).
   Proof. iIntros (?[|]?[|[[]|][]]) "? //". by iExists _. Qed.
diff --git a/theories/typing/product.v b/theories/typing/product.v
index 37a9c6bac1e6fd7ae867f46a2c06a95351b0576d..0cb50dac68d6e75ee7fafd0a6a0d81d23c42fc50 100644
--- a/theories/typing/product.v
+++ b/theories/typing/product.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From iris.algebra Require Import list numbers.
 From lrust.typing Require Import lft_contexts.
 From lrust.typing Require Export type.
@@ -290,7 +290,7 @@ Section typing.
   Hint Resolve prod_resolve : lrust_typing.
   Lemma xprod_resolve {𝔄l} (tyl: typel 𝔄l) Φl E L :
     resolvel E L tyl Φl →
-    resolve E L (Π! tyl) (λ al, pforall (λ _, curry ($)) (pzip Φl al)).
+    resolve E L (Π! tyl) (λ al, pforall (λ _, uncurry ($)) (pzip Φl al)).
   Proof.
     elim; [eapply resolve_impl; [apply resolve_just|done]|]=>/= *.
     by eapply resolve_impl; [solve_typing|]=>/= [[??][??]].
@@ -424,7 +424,7 @@ Section typing.
   Qed.
 
   Lemma xprod_ty_app_prod {𝔄l 𝔅l} E L (tyl: typel 𝔄l) (tyl': typel 𝔅l) :
-    eqtype E L (Π! (tyl h++ tyl')) (Π! tyl * Π! tyl') psep (curry papp).
+    eqtype E L (Π! (tyl h++ tyl')) (Π! tyl * Π! tyl') psep (uncurry papp).
   Proof.
     elim: tyl=> [|> Eq].
     - eapply eqtype_eq.
diff --git a/theories/typing/product_split.v b/theories/typing/product_split.v
index a941995dcf8c73fd4b6ef05498437a182c476af0..707e54acc5639985b2e98b24d766132e627ba274 100644
--- a/theories/typing/product_split.v
+++ b/theories/typing/product_split.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From lrust.typing Require Export type.
 From lrust.typing Require Import type_context lft_contexts product own uniq_bor.
 From lrust.typing Require Import shr_bor mod_ty uninit.
diff --git a/theories/typing/soundness.v b/theories/typing/soundness.v
index 9fe2981cb7d4c0e4ab537f724a5bdb5ddaf1c8d9..c86c4f30474c5a6df0320add7908887400dfbff6 100644
--- a/theories/typing/soundness.v
+++ b/theories/typing/soundness.v
@@ -1,14 +1,14 @@
 From iris.algebra Require Import frac.
 From iris.base_logic.lib Require Import na_invariants.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From lrust.lang Require Import races adequacy proofmode notation.
 From lrust.lifetime Require Import lifetime frac_borrow.
 From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
 Class typePreG Σ := PreTypeG {
-  type_preG_lrustG :> lrustPreG Σ;
-  type_preG_lftG :> lftPreG Σ;
+  type_preG_lrustGS :> lrustGpreS Σ;
+  type_preG_lftGS :> lftGpreS Σ;
   type_preG_na_invG :> na_invG Σ;
   type_preG_frac_borG :> frac_borG Σ;
   type_preG_prophG:> prophPreG Σ;
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index 2044502624d0f7022dcf9989af20eb809d58181d..0d0f09f97c5fa5e2da78300351b2d45f54f2c407 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From lrust.typing Require Import lft_contexts mod_ty.
 From lrust.typing Require Export type.
 Set Default Proof Using "Type".
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 01e735e5a171d519311988eb69f42f1bbf055da3..401d5979bbc7506483b2ac7eaace080f48e2fabe 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -11,10 +11,10 @@ Set Default Proof Using "Type".
 Implicit Type (𝔄 𝔅 ℭ: syn_type) (𝔄l 𝔅l: syn_typel).
 
 Class typeG Σ := TypeG {
-  type_lrustG :> lrustG Σ;
+  type_lrustGS :> lrustGS Σ;
   type_prophG :> prophG Σ;
   type_uniqG :> uniqG Σ;
-  type_lftG :> lftG Σ;
+  type_lftGS :> lftGS Σ;
   type_na_invG :> na_invG Σ;
   type_frac_borG :> frac_borG Σ;
 }.
@@ -121,7 +121,7 @@ Proof.
 Qed.
 
 Lemma elctx_interp_ty_outlives_E `{!typeG Σ} {𝔄} (ty: type 𝔄) α :
-  elctx_interp (ty_outlives_E ty α) ⊣⊢ α ⊑ ty.(ty_lft).
+  elctx_interp (ty_outlives_E ty α) ⊣⊢ α ⊑ ty_lft ty.
 Proof.
   rewrite /ty_outlives_E /elctx_elt_interp big_sepL_fmap /=.
   elim ty.(ty_lfts)=>/= [|κ l ->].
@@ -453,12 +453,12 @@ Ltac solve_ne_type :=
 
 Inductive TypeLftMorphism `{!typeG Σ} {𝔄 𝔅} (T: type 𝔄 → type 𝔅) : Prop :=
 | type_lft_morphism_add α βs E :
-    (∀ty, ⊢ (T ty).(ty_lft) ≡ₗ α ⊓ ty.(ty_lft)) →
+    (∀ty, ⊢ ty_lft (T ty) ≡ₗ α ⊓ ty_lft ty) →
     (∀ty, elctx_interp (T ty).(ty_E) ⊣⊢
-      elctx_interp E ∗ elctx_interp ty.(ty_E) ∗ [∗ list] β ∈ βs, β ⊑ ty.(ty_lft)) →
+      elctx_interp E ∗ elctx_interp ty.(ty_E) ∗ [∗ list] β ∈ βs, β ⊑ ty_lft ty) →
     TypeLftMorphism T
 | type_lft_morphism_const α E :
-    (∀ty, ⊢ (T ty).(ty_lft) ≡ₗ α) →
+    (∀ty, ⊢ ty_lft (T ty) ≡ₗ α) →
     (∀ty, elctx_interp (T ty).(ty_E) ⊣⊢ elctx_interp E) →
     TypeLftMorphism T.
 Existing Class TypeLftMorphism.
@@ -516,7 +516,7 @@ Qed.
 
 Lemma type_lft_morphism_lft_equiv_proper {𝔄 𝔅} (T: type 𝔄 → type 𝔅)
   {HT: TypeLftMorphism T} ty ty' :
-  ty.(ty_lft) ≡ₗ ty'.(ty_lft) -∗ (T ty).(ty_lft) ≡ₗ (T ty').(ty_lft).
+  ty_lft ty ≡ₗ ty_lft ty' -∗ ty_lft (T ty) ≡ₗ ty_lft (T ty').
 Proof.
   iIntros "#?". case HT=> [α βs E Hα HE|α E Hα HE].
   - iApply lft_equiv_trans; [|iApply lft_equiv_sym; iApply Hα].
@@ -528,7 +528,7 @@ Qed.
 
 Lemma type_lft_morphism_elctx_interp_proper {𝔄 𝔅} (T: type 𝔄 → type 𝔅)
   {HT: TypeLftMorphism T} ty ty' :
-  elctx_interp ty.(ty_E) ≡ elctx_interp ty'.(ty_E) → (⊢ ty.(ty_lft) ≡ₗ ty'.(ty_lft)) →
+  elctx_interp ty.(ty_E) ≡ elctx_interp ty'.(ty_E) → (⊢ ty_lft ty ≡ₗ ty_lft ty') →
   elctx_interp (T ty).(ty_E) ≡ elctx_interp (T ty').(ty_E).
 Proof.
   move=> EqvE EqvLft. move: HT=> [|] > ? HE; [|by rewrite !HE].
@@ -541,13 +541,13 @@ Class TypeNonExpansive `{!typeG Σ} {𝔄 𝔅} (T: type 𝔄 → type 𝔅) : P
   type_ne_ty_size ty ty' :
     ty.(ty_size) = ty'.(ty_size) → (T ty).(ty_size) = (T ty').(ty_size);
   type_ne_ty_own n ty ty' :
-    ty.(ty_size) = ty'.(ty_size) → (⊢ ty.(ty_lft) ≡ₗ ty'.(ty_lft)) →
+    ty.(ty_size) = ty'.(ty_size) → (⊢ ty_lft ty ≡ₗ ty_lft ty') →
     elctx_interp ty.(ty_E) ≡ elctx_interp ty'.(ty_E) →
     (∀vπ d tid vl, ty.(ty_own) vπ d tid vl ≡{n}≡ ty'.(ty_own) vπ d tid vl) →
     (∀vπ d κ tid l, ty.(ty_shr) vπ d κ tid l ≡{S n}≡ ty'.(ty_shr) vπ d κ tid l) →
     (∀vπ d tid vl, (T ty).(ty_own) vπ d tid vl ≡{n}≡ (T ty').(ty_own) vπ d tid vl);
   type_ne_ty_shr n ty ty' :
-    ty.(ty_size) = ty'.(ty_size) → (⊢ ty.(ty_lft) ≡ₗ ty'.(ty_lft)) →
+    ty.(ty_size) = ty'.(ty_size) → (⊢ ty_lft ty ≡ₗ ty_lft ty') →
     elctx_interp ty.(ty_E) ≡ elctx_interp ty'.(ty_E) →
     (∀vπ d tid vl,
       dist_later n (ty.(ty_own) vπ d tid vl) (ty'.(ty_own) vπ d tid vl)) →
@@ -559,13 +559,13 @@ Class TypeContractive `{!typeG Σ} {𝔄 𝔅} (T: type 𝔄 → type 𝔅) : Pr
   type_contractive_type_lft_morphism : TypeLftMorphism T;
   type_contractive_ty_size ty ty' : (T ty).(ty_size) = (T ty').(ty_size);
   type_contractive_ty_own n ty ty' :
-    ty.(ty_size) = ty'.(ty_size) → (⊢ ty.(ty_lft) ≡ₗ ty'.(ty_lft)) →
+    ty.(ty_size) = ty'.(ty_size) → (⊢ ty_lft ty ≡ₗ ty_lft ty') →
     elctx_interp ty.(ty_E) ≡ elctx_interp ty'.(ty_E) →
     (∀vπ d tid vl, dist_later n (ty.(ty_own) vπ d tid vl) (ty'.(ty_own) vπ d tid vl)) →
     (∀vπ d κ tid l, ty.(ty_shr) vπ d κ tid l ≡{n}≡ ty'.(ty_shr) vπ d κ tid l) →
     (∀vπ d tid vl, (T ty).(ty_own) vπ d tid vl ≡{n}≡ (T ty').(ty_own) vπ d tid vl);
   type_contractive_ty_shr n ty ty' :
-    ty.(ty_size) = ty'.(ty_size) → (⊢ ty.(ty_lft) ≡ₗ ty'.(ty_lft)) →
+    ty.(ty_size) = ty'.(ty_size) → (⊢ ty_lft ty ≡ₗ ty_lft ty') →
     elctx_interp ty.(ty_E) ≡ elctx_interp ty'.(ty_E) →
     (∀vπ d tid vl, match n with S (S n) =>
       ty.(ty_own) vπ d tid vl ≡{n}≡ ty'.(ty_own) vπ d tid vl | _ => True end) →
@@ -867,7 +867,7 @@ End real.
 
 Definition type_incl `{!typeG Σ} {𝔄 𝔅} (ty: type 𝔄) (ty': type 𝔅) (f: 𝔄 → 𝔅)
   : iProp Σ :=
-  ⌜ty.(ty_size) = ty'.(ty_size)⌝ ∗ (ty'.(ty_lft) ⊑ ty.(ty_lft)) ∗
+  ⌜ty.(ty_size) = ty'.(ty_size)⌝ ∗ (ty_lft ty' ⊑ ty_lft ty) ∗
   (□ ∀vπ d tid vl, ty.(ty_own) vπ d tid vl -∗ ty'.(ty_own) (f ∘ vπ) d tid vl) ∗
   (□ ∀vπ d κ tid l, ty.(ty_shr) vπ d κ tid l -∗ ty'.(ty_shr) (f ∘ vπ) d κ tid l).
 Instance: Params (@type_incl) 4 := {}.
@@ -900,7 +900,7 @@ Section subtyping.
   Lemma eqtype_unfold {𝔄 𝔅} E L f g `{!Iso f g} (ty : type 𝔄) (ty' : type 𝔅) :
     eqtype E L ty ty' f g ↔
     ∀qL, llctx_interp L qL -∗ □ (elctx_interp E -∗
-      ⌜ty.(ty_size) = ty'.(ty_size)⌝ ∗ ty.(ty_lft) ≡ₗ ty'.(ty_lft) ∗
+      ⌜ty.(ty_size) = ty'.(ty_size)⌝ ∗ ty_lft ty ≡ₗ ty_lft ty' ∗
       (□ ∀vπ d tid vl, ty.(ty_own) vπ d tid vl ↔ ty'.(ty_own) (f ∘ vπ) d tid vl) ∗
       (□ ∀vπ d κ tid l, ty.(ty_shr) vπ d κ tid l ↔ ty'.(ty_shr) (f ∘ vπ) d κ tid l)).
   Proof.
@@ -924,7 +924,7 @@ Section subtyping.
   Lemma eqtype_id_unfold {𝔄} E L (ty ty': type 𝔄) :
     eqtype E L ty ty' id id ↔
     ∀qL, llctx_interp L qL -∗ □ (elctx_interp E -∗
-      ⌜ty.(ty_size) = ty'.(ty_size)⌝ ∗ ty.(ty_lft) ≡ₗ ty'.(ty_lft) ∗
+      ⌜ty.(ty_size) = ty'.(ty_size)⌝ ∗ ty_lft ty ≡ₗ ty_lft ty' ∗
       (□ ∀vπ d tid vl, ty.(ty_own) vπ d tid vl ↔ ty'.(ty_own) vπ d tid vl) ∗
       (□ ∀vπ d κ tid l, ty.(ty_shr) vπ d κ tid l ↔ ty'.(ty_shr) vπ d κ tid l)).
   Proof. by rewrite eqtype_unfold. Qed.
@@ -1058,7 +1058,7 @@ Section subtyping.
   (** Simple Type *)
 
   Lemma type_incl_simple_type {𝔄 𝔅} f (st: simple_type 𝔄) (st': simple_type 𝔅):
-    st.(st_size) = st'.(st_size) → st'.(ty_lft) ⊑ st.(ty_lft) -∗
+    st.(st_size) = st'.(st_size) → ty_lft st' ⊑ ty_lft st -∗
     □ (∀vπ d tid vl, st.(st_own) vπ d tid vl -∗ st'.(st_own) (f ∘ vπ) d tid vl) -∗
     type_incl st st' f.
   Proof.
@@ -1069,7 +1069,7 @@ Section subtyping.
 
   Lemma subtype_simple_type {𝔄 𝔅} E L f (st: simple_type 𝔄) (st': simple_type 𝔅) :
     (∀qL, llctx_interp L qL -∗ □ (elctx_interp E -∗
-      ⌜st.(st_size) = st'.(st_size)⌝ ∗ st'.(ty_lft) ⊑ st.(ty_lft) ∗
+      ⌜st.(st_size) = st'.(st_size)⌝ ∗ ty_lft st' ⊑ ty_lft st ∗
       (∀vπ d tid vl, st.(st_own) vπ d tid vl -∗ st'.(st_own) (f ∘ vπ) d tid vl))) →
     subtype E L st st' f.
   Proof.
@@ -1081,7 +1081,7 @@ Section subtyping.
   (** Plain Type *)
 
   Lemma type_incl_plain_type {𝔄 𝔅} f (pt: plain_type 𝔄) (pt': plain_type 𝔅):
-    pt.(pt_size) = pt'.(pt_size) → pt'.(ty_lft) ⊑ pt.(ty_lft) -∗
+    pt.(pt_size) = pt'.(pt_size) → ty_lft pt' ⊑ ty_lft pt -∗
     □ (∀v tid vl, pt.(pt_own) v tid vl -∗ pt'.(pt_own) (f v) tid vl) -∗
     type_incl pt pt' f.
   Proof.
@@ -1093,7 +1093,7 @@ Section subtyping.
 
   Lemma subtype_plain_type {𝔄 𝔅} E L f (pt: plain_type 𝔄) (pt': plain_type 𝔅) :
     (∀qL, llctx_interp L qL -∗ □ (elctx_interp E -∗
-      ⌜pt.(pt_size) = pt'.(pt_size)⌝ ∗ pt'.(ty_lft) ⊑ pt.(ty_lft) ∗
+      ⌜pt.(pt_size) = pt'.(pt_size)⌝ ∗ ty_lft pt' ⊑ ty_lft pt ∗
       (∀v tid vl, pt.(pt_own) v tid vl -∗ pt'.(pt_own) (f v) tid vl))) →
     subtype E L pt pt' f.
   Proof.
diff --git a/theories/typing/type_context.v b/theories/typing/type_context.v
index 02623ad5942af159dbe15e7f7a133adaeb6eb387..a643d73273ad12eefb09af301aa70ac9b8691a45 100644
--- a/theories/typing/type_context.v
+++ b/theories/typing/type_context.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From lrust.typing Require Import type lft_contexts.
 Set Default Proof Using "Type".
 
@@ -64,7 +64,7 @@ Section type_context.
     | e => to_val e end.
 
   Lemma eval_path_of_val (v: val) : eval_path v = Some v.
-  Proof. case v; [done|]=>/= *. by rewrite (decide_left _). Qed.
+  Proof. case v; [done|]=>/= *. by rewrite (decide_True_pi _). Qed.
 
   Lemma wp_eval_path E p v :
     eval_path p = Some v → ⊢ WP p @ E {{ v', ⌜v' = v⌝ }}.
@@ -538,7 +538,7 @@ Section lemmas.
   Qed.
 
   Lemma unblock_tctx_cons_unblock {𝔄 𝔄l} p (ty: type 𝔄) (T T': tctx 𝔄l) κ E L :
-    lctx_lft_alive E L ty.(ty_lft) → unblock_tctx E L κ T T' →
+    lctx_lft_alive E L (ty_lft ty) → unblock_tctx E L κ T T' →
     unblock_tctx E L κ (p ◁{κ} ty +:: T) (p ◁ ty +:: T').
   Proof.
     iIntros (Alv Un ??[??]) "#LFT #E [L L'] #†κ /=[(%v &%& Upd) T]".
diff --git a/theories/typing/type_sum.v b/theories/typing/type_sum.v
index 2d66c2b6b24796a7328dc7b4cd743772b9fa1e57..464e99b6d006bb3521e9c4d990c53576c6925952 100644
--- a/theories/typing/type_sum.v
+++ b/theories/typing/type_sum.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From lrust.lang Require Import memcpy.
 From lrust.typing Require Import int uninit uniq_bor shr_bor own sum.
 From lrust.typing Require Import lft_contexts type_context programs product.
diff --git a/theories/typing/uniq_array_util.v b/theories/typing/uniq_array_util.v
index 702f3ff41b009b1012069f2ecff71227931df6bc..0fd1dfe3cdbbdd43f61081030bbb3dcfa52e213b 100644
--- a/theories/typing/uniq_array_util.v
+++ b/theories/typing/uniq_array_util.v
@@ -8,7 +8,7 @@ Section uniq_array_util.
 
   Lemma ty_share_big_sepL_uniq_body {𝔄} (ty: type 𝔄) n (vπξil: vec _ n)
       d κ tid l κ' q E :
-    ↑lftN ⊆ E → lft_ctx -∗ κ' ⊑ κ -∗ κ' ⊑ ty.(ty_lft) -∗
+    ↑lftN ⊆ E → lft_ctx -∗ κ' ⊑ κ -∗ κ' ⊑ ty_lft ty -∗
     &{κ'} ([∗ list] i ↦ vπξi ∈ vπξil, uniq_body ty vπξi.1 vπξi.2 d κ tid (l +ₗ[ty] i)) -∗
     q.[κ'] ={E}=∗ |={E}▷=>^(S d) |={E}=>
       let ξl := vmap (λ vπξi, PrVar (𝔄 ↾ prval_to_inh vπξi.1) vπξi.2) vπξil in
@@ -31,7 +31,7 @@ Section uniq_array_util.
 
   Lemma ty_own_proph_big_sepL_uniq_body {𝔄} (ty: type 𝔄) n (vπξil: vec _ n)
       d κ tid l κ' q E :
-    ↑lftN ⊆ E → lft_ctx -∗ κ' ⊑ κ -∗ κ' ⊑ ty.(ty_lft) -∗
+    ↑lftN ⊆ E → lft_ctx -∗ κ' ⊑ κ -∗ κ' ⊑ ty_lft ty -∗
     ([∗ list] i ↦ vπξi ∈ vπξil, uniq_body ty vπξi.1 vπξi.2 d κ tid (l +ₗ[ty] i)) -∗
     q.[κ'] ={E}=∗ |={E}▷=>^(S d) |={E}=>
       let ξl := vmap (λ vπξi, PrVar (𝔄 ↾ prval_to_inh vπξi.1) vπξi.2) vπξil in
@@ -61,7 +61,7 @@ Section uniq_array_util.
 
   Lemma resolve_big_sepL_uniq_body {𝔄} (ty: type 𝔄) n (vπξil: vec _ n) d κ tid l E L q F :
     lctx_lft_alive E L κ → ↑lftN ∪ ↑prophN ⊆ F →
-    lft_ctx -∗ proph_ctx -∗ κ ⊑ ty.(ty_lft) -∗ elctx_interp E -∗ llctx_interp L q -∗
+    lft_ctx -∗ proph_ctx -∗ κ ⊑ ty_lft ty -∗ elctx_interp E -∗ llctx_interp L q -∗
     ([∗ list] i ↦ vπξi ∈ vπξil, uniq_body ty vπξi.1 vπξi.2 d κ tid (l +ₗ[ty] i))
       ={F}=∗ |={F}▷=>^(S d) |={F}=>
       let φπ π := lforall (λ vπξi,
diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v
index e183599a735671728a2af93da7dd83a202e249fb..458c9517ff4544e3575f6c1470c9d8a89ee05379 100644
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
@@ -21,7 +21,7 @@ Section uniq_bor.
 
   Program Definition uniq_bor {𝔄} (κ: lft) (ty: type 𝔄) : type (𝔄 * 𝔄) := {|
     ty_size := 1;  ty_lfts := κ :: ty.(ty_lfts);  ty_E := ty.(ty_E) ++ ty_outlives_E ty κ;
-    ty_own vπ d tid vl := κ ⊑ ty.(ty_lft) ∗ [loc[l] := vl] ∃d' ξi,
+    ty_own vπ d tid vl := κ ⊑ ty_lft ty ∗ [loc[l] := vl] ∃d' ξi,
       let ξ := PrVar (𝔄 ↾ prval_to_inh (fst ∘ vπ)) ξi in
       ⌜(S d' ≤ d)%nat ∧ snd ∘ vπ = (.$ ξ)⌝ ∗ uniq_body ty (fst ∘ vπ) ξi d' κ tid l;
     ty_shr vπ d κ' tid l := [S(d') := d] ∃(l': loc) ξ, ⌜snd ∘ vπ ./ [ξ]⌝ ∗
@@ -107,10 +107,10 @@ Section typing.
   Qed.
 
   Global Instance uniq_send {𝔄} κ (ty: type 𝔄) : Send ty → Send (&uniq{κ} ty).
-  Proof. move=> >/=. rewrite /uniq_body. by do 19 f_equiv. Qed.
+  Proof. move=> >/=. rewrite /uniq_body. by do 19 (f_equiv || move=>?). Qed.
 
   Global Instance uniq_sync {𝔄} κ (ty: type 𝔄) : Sync ty → Sync (&uniq{κ} ty).
-  Proof. move=> >/=. by do 10 f_equiv. Qed.
+  Proof. move=> >/=. by do 10 (f_equiv || move=>?). Qed.
 
   Global Instance uniq_just_loc {𝔄} κ (ty: type 𝔄) : JustLoc (&uniq{κ} ty).
   Proof. iIntros (???[|[[]|][]]) "[_ ?] //". by iExists _. Qed.
diff --git a/theories/typing/uniq_cmra.v b/theories/typing/uniq_cmra.v
index 841f0c901a2af96a90ff65384dc9e3e06b6b0871..33dc2fb56598a7c9e0fd6c06966dc2ebbc3aa98c 100644
--- a/theories/typing/uniq_cmra.v
+++ b/theories/typing/uniq_cmra.v
@@ -1,5 +1,5 @@
-From iris.algebra Require Import auth cmra functions gmap frac_agree.
-From iris.proofmode Require Import tactics.
+From iris.algebra Require Import auth cmra functions gmap dfrac_agree.
+From iris.proofmode Require Import proofmode.
 From iris.base_logic Require Import invariants.
 From lrust.util Require Import discrete_fun.
 From lrust.prophecy Require Import prophecy.
@@ -9,7 +9,7 @@ Implicit Type (𝔄i: syn_typei) (𝔄: syn_type).
 
 (** * Camera for Unique Borrowing *)
 
-Local Definition uniq_itemR 𝔄i := frac_agreeR (leibnizO (proph 𝔄i * nat)).
+Local Definition uniq_itemR 𝔄i := dfrac_agreeR (leibnizO (proph 𝔄i * nat)).
 Local Definition uniq_gmapUR 𝔄i := gmapUR positive (uniq_itemR 𝔄i).
 Local Definition uniq_smryUR := discrete_funUR uniq_gmapUR.
 Definition uniqUR: ucmra := authUR uniq_smryUR.
@@ -32,7 +32,7 @@ Definition uniqN: namespace := lft_userN .@ "uniq".
 (** * Iris Propositions *)
 
 Section defs.
-Context `{!invG Σ, !prophG Σ, !uniqG Σ}.
+Context `{!invGS Σ, !prophG Σ, !uniqG Σ}.
 
 (** Unique Reference Context *)
 Definition uniq_inv: iProp Σ := ∃S, own uniq_name (● S).
@@ -62,7 +62,7 @@ Definition prval_to_inh {𝔄} (vπ: proph 𝔄) : inh_syn_type 𝔄 :=
   to_inh_syn_type (vπ inhabitant).
 
 Section lemmas.
-Context `{!invG Σ, !prophG Σ, !uniqG Σ}.
+Context `{!invGS Σ, !prophG Σ, !uniqG Σ}.
 
 Global Instance uniq_ctx_persistent : Persistent uniq_ctx := _.
 Global Instance val_obs_timeless ξ vπ d : Timeless (.VO[ξ] vπ d) := _.
diff --git a/theories/typing/uniq_util.v b/theories/typing/uniq_util.v
index f1182cfd40089cc3120bb70db9ba8baedb70e6a1..71ec5c50777f6653514bea46f1c6a2a944d34bfc 100644
--- a/theories/typing/uniq_util.v
+++ b/theories/typing/uniq_util.v
@@ -13,7 +13,7 @@ Section uniq_util.
     &{κ} (∃vπ' d', ⧖(S d') ∗ .PC[ξ] vπ' d' ∗ l ↦∗: ty.(ty_own) vπ' d' tid).
 
   Lemma ty_share_uniq_body {𝔄} (ty: type 𝔄) vπ ξi d κ tid l κ' q E :
-    ↑lftN ⊆ E → lft_ctx -∗ κ' ⊑ κ -∗ κ' ⊑ ty.(ty_lft) -∗
+    ↑lftN ⊆ E → lft_ctx -∗ κ' ⊑ κ -∗ κ' ⊑ ty_lft ty -∗
     &{κ'} (uniq_body ty vπ ξi d κ tid l) -∗ q.[κ'] ={E}=∗ |={E}▷=>^(S d) |={E}=>
       &{κ'} 1:[PrVar (𝔄 ↾ prval_to_inh vπ) ξi] ∗ ty.(ty_shr) vπ d κ' tid l ∗ q.[κ'].
   Proof.
@@ -37,7 +37,7 @@ Section uniq_util.
   Qed.
 
   Lemma ty_own_proph_uniq_body {𝔄} (ty: type 𝔄) vπ ξi d κ tid l κ' q E :
-    ↑lftN ⊆ E → lft_ctx -∗ κ' ⊑ κ -∗ κ' ⊑ ty.(ty_lft) -∗
+    ↑lftN ⊆ E → lft_ctx -∗ κ' ⊑ κ -∗ κ' ⊑ ty_lft ty -∗
     uniq_body ty vπ ξi d κ tid l -∗ q.[κ'] ={E}=∗ |={E}▷=>^(S d) |={E}=>
       let ξ := PrVar (𝔄 ↾ prval_to_inh vπ) ξi in
       ∃ζl q', ⌜vπ ./ ζl⌝ ∗ q':+[ζl ++ [ξ]] ∗
@@ -64,7 +64,7 @@ Section uniq_util.
 
   Lemma resolve_uniq_body {𝔄} (ty: type 𝔄) vπ ξi d κ tid l E L q F :
     lctx_lft_alive E L κ → ↑lftN ∪ ↑prophN ⊆ F →
-    lft_ctx -∗ proph_ctx -∗ κ ⊑ ty.(ty_lft) -∗ elctx_interp E -∗ llctx_interp L q -∗
+    lft_ctx -∗ proph_ctx -∗ κ ⊑ ty_lft ty -∗ elctx_interp E -∗ llctx_interp L q -∗
     uniq_body ty vπ ξi d κ tid l ={F}=∗ |={F}▷=>^(S d) |={F}=>
       ⟨π, π (PrVar (𝔄 ↾ prval_to_inh vπ) ξi) = vπ π⟩ ∗ llctx_interp L q.
   Proof.
diff --git a/theories/util/basic.v b/theories/util/basic.v
index 0d4258d5551148d88938f89436bfeaba5e7113c5..2249a47e640a1e18560943e34167d0dcd0f36421 100644
--- a/theories/util/basic.v
+++ b/theories/util/basic.v
@@ -1,6 +1,6 @@
 Require Export Equality FunctionalExtensionality.
 From iris.algebra Require Import ofe.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 
 (** * Utility for Point-Free Style *)
 
diff --git a/theories/util/fancy_lists.v b/theories/util/fancy_lists.v
index eecfa3825febbb2b41a74ac6d37cbc19cd36e6ff..2f09d7594664f78790d7a03d7292af3ed2cd957e 100644
--- a/theories/util/fancy_lists.v
+++ b/theories/util/fancy_lists.v
@@ -1,5 +1,5 @@
 From iris.algebra Require Import ofe.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From lrust.util Require Import basic.
 
 (** * Heterogeneous List *)
@@ -154,7 +154,7 @@ Fixpoint plookup {Xl} (xl: plist Xl) : ∀i, F (Xl !!ₗ i) :=
   end.
 
 Global Instance papp_psep_iso {Xl Yl}
-  : Iso (curry (@papp Xl Yl)) (λ xl, (psepl xl, psepr xl)).
+  : Iso (uncurry (@papp Xl Yl)) (λ xl, (psepl xl, psepr xl)).
 Proof.
   split; fun_ext.
   - case=>/= [??]. by rewrite papp_sepl papp_sepr.
@@ -704,7 +704,7 @@ Lemma big_sepHL_2_big_sepN {F G H: A → Type} {Xl}
   [∗ nat] i < length Xl, Φ _ (xl +!! i) (yl -!! i) (zl -!! i).
 Proof.
   move: Φ. induction Xl; inv_hlist xl; case yl; case zl; [done|]=>/= *.
-  f_equiv. apply IHXl.
+  f_equiv; [done|apply IHXl].
 Qed.
 
 Lemma big_sepHL_2_lookup {F G H: A → Type} {Xl}
diff --git a/theories/util/update.v b/theories/util/update.v
index 92338ce213dfd1eeda40d696a262dda95fdc93c4..6b4e1911f101b02626cd78e6ccb10ea4a5b10083 100644
--- a/theories/util/update.v
+++ b/theories/util/update.v
@@ -1,5 +1,5 @@
 From iris.bi Require Import updates.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From lrust.util Require Import basic.
 
 (* TODO : move all that to Iris *)
diff --git a/theories/util/vector.v b/theories/util/vector.v
index 01f4ef89115ce3008105952a93d5cb03cdecf83a..95107ddfa268a0cdc2d35cc0b5a2c86433a526e3 100644
--- a/theories/util/vector.v
+++ b/theories/util/vector.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import proofmode.
 From lrust.util Require Import basic.
 
 (* TODO : move all that to stdpp *)
@@ -25,7 +25,7 @@ Global Instance vhd_vsingleton_iso {A} : Iso vhd (λ x: A, [#x]).
 Proof. split; [|done]. fun_ext=> v. by inv_vec v. Qed.
 
 Global Instance vhd_vtl_vcons_iso {A n} :
-  Iso (λ v: vec A (S n), (vhd v, vtl v)) (curry vcons').
+  Iso (λ v: vec A (S n), (vhd v, vtl v)) (uncurry vcons').
 Proof. split; fun_ext; [|by case]=> v. by inv_vec v. Qed.
 
 Global Instance vec_to_list_inj' {A n} : Inj (=) (=) (@vec_to_list A n).
@@ -52,7 +52,7 @@ Qed.
 Lemma vapp_ex {A m n} (xl: _ A (m + n)) : ∃yl zl, xl = yl +++ zl.
 Proof. eexists _, _. apply vsepat_app. Qed.
 
-Global Instance vapp_vsepat_iso {A} m n : Iso (curry vapp) (@vsepat A m n).
+Global Instance vapp_vsepat_iso {A} m n : Iso (uncurry vapp) (@vsepat A m n).
 Proof.
   split; fun_ext.
   - move=> [xl ?]. by elim xl; [done|]=>/= ???->.