diff --git a/theories/lifetime/accessors.v b/theories/lifetime/accessors.v
index 46895ee80e4b9e90654e0074b8b424ac4631754b..14210f73bc4106af113f0cdeb202146fc30440aa 100644
--- a/theories/lifetime/accessors.v
+++ b/theories/lifetime/accessors.v
@@ -1,6 +1,6 @@
 From lrust.lifetime Require Export primitive.
 From iris.proofmode Require Import tactics.
-From iris.algebra Require Import csum auth frac gmap dec_agree gset.
+From iris.algebra Require Import csum auth frac gmap agree gset.
 From iris.base_logic Require Import big_op.
 From iris.base_logic.lib Require Import boxes.
 
@@ -14,7 +14,7 @@ Lemma bor_open_internal E P i Pb q :
   slice borN (i.2) P -∗ ▷ lft_bor_alive (i.1) Pb -∗
   idx_bor_own 1%Qp i -∗ (q).[i.1] ={E}=∗
     ▷ lft_bor_alive (i.1) Pb ∗
-    own_bor (i.1) (◯ {[i.2 := (1%Qp, DecAgree (Bor_open q))]}) ∗ ▷ P.
+    own_bor (i.1) (◯ {[i.2 := (1%Qp, to_agree (Bor_open q))]}) ∗ ▷ P.
 Proof.
   iIntros (?) "Hslice Halive Hbor Htok". unfold lft_bor_alive, idx_bor_own.
   iDestruct "Halive" as (B) "(Hbox & >Hown & HB)".
@@ -25,7 +25,7 @@ Proof.
   rewrite -(fmap_insert bor_filled _ _ (Bor_open q)).
   iMod (own_bor_update_2 with "Hown Hbor") as "Hbor". apply auth_update.
   { eapply singleton_local_update. by rewrite lookup_fmap EQB.
-    by apply (exclusive_local_update _ (1%Qp, DecAgree (Bor_open q))). }
+    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.
@@ -35,7 +35,7 @@ Qed.
 Lemma bor_close_internal E P i Pb q :
   ↑borN ⊆ E →
   slice borN (i.2) P -∗ ▷ lft_bor_alive (i.1) Pb -∗
-  own_bor (i.1) (◯ {[i.2 := (1%Qp, DecAgree (Bor_open q))]}) -∗ ▷ P ={E}=∗
+  own_bor (i.1) (◯ {[i.2 := (1%Qp, to_agree (Bor_open q))]}) -∗ ▷ P ={E}=∗
     ▷ lft_bor_alive (i.1) Pb ∗ idx_bor_own 1%Qp i ∗ (q).[i.1].
 Proof.
   iIntros (?) "Hslice Halive Hbor HP". unfold lft_bor_alive, idx_bor_own.
@@ -47,7 +47,7 @@ Proof.
   rewrite -(fmap_insert bor_filled _ _ Bor_in).
   iMod (own_bor_update_2 with "Hown Hbor") as "Hbor". apply auth_update.
   { eapply singleton_local_update. by rewrite lookup_fmap EQB.
-    by apply (exclusive_local_update _ (1%Qp, DecAgree Bor_in)). }
+    by apply (exclusive_local_update _ (1%Qp, to_agree Bor_in)). }
   rewrite own_bor_op -fmap_insert. iDestruct "Hbor" as "[Hown $]".
   rewrite big_sepM_delete //. simpl. iDestruct "HB" as "[>$ HB]".
   iExists _. iFrame "Hbox Hown".
@@ -103,7 +103,7 @@ Proof.
       iDestruct (own_bor_valid_2 with "Hinv Hf")
         as %[(_ & <- & INCL%option_included)%singleton_included _]%auth_valid_discrete_2.
       by destruct INCL as [[=]|(? & ? & [=<-] &
-        [[_<-]%lookup_to_gmap_Some [[_[=]]|[]%(exclusive_included _)]])].
+        [[_<-]%lookup_to_gmap_Some [[_ ?%(inj to_agree)]|[]%(exclusive_included _)]])].
   - iMod (lft_dead_in_tok with "HA") as "[_ H†]". done.
     iDestruct (lft_tok_dead with "Htok H†") as "[]".
 Qed.
@@ -181,7 +181,7 @@ Proof.
       { apply auth_update. etrans.
         - apply delete_singleton_local_update, _.
         - apply (alloc_singleton_local_update _ j
-                   (1%Qp, DecAgree (Bor_open q'))); last done.
+                   (1%Qp, to_agree (Bor_open q'))); last done.
           rewrite -fmap_delete lookup_fmap fmap_None
                   -fmap_None -lookup_fmap fmap_delete //. }
       rewrite own_bor_op. iDestruct "Hown" as "[Hown Hbor]".
@@ -200,7 +200,7 @@ Proof.
       iDestruct (own_bor_valid_2 with "Hinv Hbor")
         as %[(_ & <- & INCL%option_included)%singleton_included _]%auth_valid_discrete_2.
       by destruct INCL as [[=]|(? & ? & [=<-] &
-        [[_<-]%lookup_to_gmap_Some [[_[=]]|[]%(exclusive_included _)]])].
+        [[_<-]%lookup_to_gmap_Some [[_?%(inj to_agree)]|[]%(exclusive_included _)]])].
   - iMod (lft_dead_in_tok with "HA") as "[_ H†]". done.
     iDestruct (lft_tok_dead with "Htok H†") as "[]".
 Qed.
@@ -234,7 +234,7 @@ Proof.
     iMod (own_bor_update_2 with "Hown Hbor") as "Hown".
     { apply auth_update. etrans.
       - apply delete_singleton_local_update, _.
-      - apply (alloc_singleton_local_update _ j (1%Qp, DecAgree (Bor_in))); last done.
+      - apply (alloc_singleton_local_update _ j (1%Qp, to_agree (Bor_in))); last done.
         rewrite -fmap_delete lookup_fmap fmap_None
                 -fmap_None -lookup_fmap fmap_delete //. }
     rewrite own_bor_op. iDestruct "Hown" as "[H● H◯]".
diff --git a/theories/lifetime/borrow.v b/theories/lifetime/borrow.v
index 3f036e8cb2e2a1768af5bf1400428f17d38143bb..e0927db166a62743512b439e5923f5898e7d4469 100644
--- a/theories/lifetime/borrow.v
+++ b/theories/lifetime/borrow.v
@@ -1,6 +1,6 @@
 From lrust.lifetime Require Export primitive.
 From lrust.lifetime Require Export faking raw_reborrow.
-From iris.algebra Require Import csum auth frac gmap dec_agree gset.
+From iris.algebra Require Import csum auth frac gmap agree gset.
 From iris.base_logic Require Import big_op.
 From iris.base_logic.lib Require Import boxes.
 From iris.proofmode Require Import tactics.
@@ -30,8 +30,8 @@ Proof.
     rewrite -(fmap_insert bor_filled _ _ Bor_in).
     iMod (own_bor_update with "HownB") as "[HB● HB◯]".
     { eapply auth_update_alloc,
-        (alloc_singleton_local_update _ γB (1%Qp, DecAgree Bor_in)); last done.
-      rewrite lookup_fmap. by destruct (B !! γB). }
+        (alloc_singleton_local_update _ γB (1%Qp, to_agree Bor_in)); last done.
+      rewrite lookup_fmap. case:(B !! γB) HBlookup; done. }
     rewrite -fmap_insert.
     iSpecialize ("Hclose'" with "[Hvs Hinh HboxB HB● HB]").
     { iNext. rewrite /lft_inv. iLeft. iFrame "%".
@@ -89,12 +89,12 @@ Proof.
     { etrans; last etrans.
       - apply auth_update_dealloc. by apply delete_singleton_local_update, _.
       - apply auth_update_alloc,
-           (alloc_singleton_local_update _ γ1 (1%Qp, DecAgree Bor_in)); last done.
+           (alloc_singleton_local_update _ γ1 (1%Qp, to_agree Bor_in)); last done.
         rewrite /to_borUR -fmap_delete lookup_fmap fmap_None
                 -fmap_None -lookup_fmap fmap_delete //.
       - apply cmra_update_op; last done.
         apply auth_update_alloc,
-          (alloc_singleton_local_update _ γ2 (1%Qp, DecAgree Bor_in)); last done.
+          (alloc_singleton_local_update _ γ2 (1%Qp, to_agree Bor_in)); last done.
         rewrite lookup_insert_ne // /to_borUR -fmap_delete lookup_fmap fmap_None
                 -fmap_None -lookup_fmap fmap_delete //. }
     rewrite !own_bor_op. iDestruct "Hbor" as "[[H● H◯2] H◯1]".
@@ -158,7 +158,7 @@ Proof.
         apply auth_update_dealloc. by apply delete_singleton_local_update, _.
       - apply auth_update_dealloc. by apply delete_singleton_local_update, _.
       - apply auth_update_alloc,
-           (alloc_singleton_local_update _ γ (1%Qp, DecAgree Bor_in)); last done.
+           (alloc_singleton_local_update _ γ (1%Qp, to_agree Bor_in)); last done.
         rewrite /to_borUR -!fmap_delete lookup_fmap fmap_None
                 -fmap_None -lookup_fmap !fmap_delete //. }
     rewrite own_bor_op. iDestruct "Hbor" as "[H● H◯]".
@@ -170,9 +170,9 @@ Proof.
     iApply "Hclose'". iLeft. iFrame "%". iExists Pb, Pi. iFrame. iExists _.
     rewrite /to_borUR -!fmap_delete -!fmap_insert. iFrame "Hbox H●".
     rewrite !big_sepM_insert /=.
-    + rewrite (big_sepM_delete _ _ _ _ EQB1) /=.
-      rewrite (big_sepM_delete _ _ j2 Bor_in) /=. by iDestruct "HB" as "[_ $]".
-      rewrite lookup_delete_ne //.
+    + rewrite (big_sepM_delete _ _ _ _ EQB1) /=. iNext. simpl.
+      rewrite [([∗ map] _ ∈ delete _ _, _)%I](big_sepM_delete _ _ j2 Bor_in) /=.
+      by iDestruct "HB" as "[_ $]". rewrite lookup_delete_ne //.
     + rewrite -fmap_None -lookup_fmap !fmap_delete //.
   - iDestruct "Hinv" as (Pinh) "(Hdead & Hcnt & Hinh)".
     iMod (raw_bor_fake _ true with "Hdead") as "[Hdead Hbor]"; first solve_ndisj.
diff --git a/theories/lifetime/creation.v b/theories/lifetime/creation.v
index b48c4cc52fb5a3ae3fd49046cf8d93607c036e77..5c4cb539aaddee477216f21653a3b4ec9af09581 100644
--- a/theories/lifetime/creation.v
+++ b/theories/lifetime/creation.v
@@ -1,6 +1,6 @@
 From lrust.lifetime Require Export primitive.
 From lrust.lifetime Require Import faking.
-From iris.algebra Require Import csum auth frac gmap dec_agree gset.
+From iris.algebra Require Import csum auth frac gmap agree gset.
 From iris.base_logic Require Import big_op.
 From iris.base_logic.lib Require Import boxes.
 From iris.proofmode Require Import tactics.
@@ -42,7 +42,7 @@ Proof.
   iMod ("Hvs" $! I with "[HI Halive Hbox Hbor] HP Hκ") as "(Hinv & HQ & Hcnt')".
   { rewrite lft_vs_inv_unfold. iFrame. rewrite /lft_bor_dead.
     iExists (dom _ B), P. rewrite !to_gmap_dom -map_fmap_compose.
-    rewrite (map_fmap_ext _ ((1%Qp,) ∘ DecAgree) B); last naive_solver.
+    rewrite (map_fmap_ext _ ((1%Qp,) ∘ to_agree) B); last naive_solver.
     iFrame. }
   rewrite lft_vs_inv_unfold; iDestruct "Hinv" as "(?&HI&Halive)".
   iSpecialize ("Halive'" with "Halive").
@@ -198,7 +198,7 @@ Proof.
       apply lft_alive_in_insert_false; last done.
       assert (κ ∉ K). intros ?. eapply H5. 2: eauto. rewrite elem_of_union. eauto.
       move: H7. rewrite elem_of_kill_set not_and_l. intros [?|?]. done.
-contradict H7. apply elem_of_dom. set_solver +HI Hκ.
+      contradict H7. apply elem_of_dom. set_solver +HI Hκ.
     + iRight. iFrame. iPureIntro. by apply lft_dead_in_insert_false.
 Qed.
 End creation.
diff --git a/theories/lifetime/definitions.v b/theories/lifetime/definitions.v
index 995a2fb3d3f0439feb92902d31792376b2eaf8d6..f93130b6886e66342ca4e022c129a4de784c16a2 100644
--- a/theories/lifetime/definitions.v
+++ b/theories/lifetime/definitions.v
@@ -1,4 +1,4 @@
-From iris.algebra Require Import csum auth frac gmap dec_agree gset.
+From iris.algebra Require Import csum auth frac gmap agree gset.
 From iris.prelude Require Export gmultiset strings.
 From iris.base_logic.lib Require Export invariants.
 From iris.base_logic.lib Require Import boxes.
@@ -20,6 +20,7 @@ Inductive bor_state :=
   | Bor_rebor (κ : lft).
 Instance bor_state_eq_dec : EqDecision bor_state.
 Proof. solve_decision. Defined.
+Canonical bor_stateC := leibnizC bor_state.
 
 Definition bor_filled (s : bor_state) : bool :=
   match s with Bor_in => true | _ => false end.
@@ -35,15 +36,16 @@ Record lft_names := LftNames {
 }.
 Instance lft_names_eq_dec : EqDecision lft_names.
 Proof. solve_decision. Defined.
+Canonical lft_namesC := leibnizC lft_names.
 
 Definition alftUR := gmapUR atomic_lft lft_stateR.
 Definition to_alftUR : gmap atomic_lft bool → alftUR := fmap to_lft_stateR.
 
-Definition ilftUR := gmapUR lft (dec_agreeR lft_names).
-Definition to_ilftUR : gmap lft lft_names → ilftUR := fmap DecAgree.
+Definition ilftUR := gmapUR lft (agreeR lft_namesC).
+Definition to_ilftUR : gmap lft lft_names → ilftUR := fmap to_agree.
 
-Definition borUR := gmapUR slice_name (prodR fracR (dec_agreeR bor_state)).
-Definition to_borUR : gmap slice_name bor_state → borUR := fmap ((1%Qp,) ∘ DecAgree).
+Definition borUR := gmapUR slice_name (prodR fracR (agreeR bor_stateC)).
+Definition to_borUR : gmap slice_name bor_state → borUR := fmap ((1%Qp,) ∘ to_agree).
 
 Definition inhUR := gset_disjUR slice_name.
 
@@ -53,9 +55,9 @@ Class lftG Σ := LftG {
   alft_name : gname;
   ilft_inG :> inG Σ (authR ilftUR);
   ilft_name : gname;
-  lft_bor_box :> inG Σ (authR borUR);
+  lft_bor_inG :> inG Σ (authR borUR);
   lft_cnt_inG :> inG Σ (authR natUR);
-  lft_inh_box :> inG Σ (authR inhUR);
+  lft_inh_inG :> inG Σ (authR inhUR);
 }.
 
 Section defs.
@@ -73,19 +75,19 @@ Section defs.
     own ilft_name (● to_ilftUR I).
 
   Definition own_bor (κ : lft)
-      (x : auth (gmap slice_name (frac * dec_agree bor_state))) : iProp Σ :=
+      (x : authR borUR) : iProp Σ :=
     (∃ γs,
-      own ilft_name (◯ {[ κ := DecAgree γs ]}) ∗
+      own ilft_name (◯ {[ κ := to_agree γs ]}) ∗
       own (bor_name γs) x)%I.
 
-  Definition own_cnt (κ : lft) (x : auth nat) : iProp Σ :=
+  Definition own_cnt (κ : lft) (x : authR natUR) : iProp Σ :=
     (∃ γs,
-      own ilft_name (◯ {[ κ := DecAgree γs ]}) ∗
+      own ilft_name (◯ {[ κ := to_agree γs ]}) ∗
       own (cnt_name γs) x)%I.
 
-  Definition own_inh (κ : lft) (x : auth (gset_disj slice_name)) : iProp Σ :=
+  Definition own_inh (κ : lft) (x : authR inhUR) : iProp Σ :=
     (∃ γs,
-      own ilft_name (◯ {[ κ := DecAgree γs ]}) ∗
+      own ilft_name (◯ {[ κ := to_agree γs ]}) ∗
       own (inh_name γs) x)%I.
 
   Definition bor_cnt (κ : lft) (s : bor_state) : iProp Σ :=
@@ -103,7 +105,7 @@ Section defs.
 
   Definition lft_bor_dead (κ : lft) : iProp Σ :=
      (∃ (B: gset slice_name) (Pb : iProp Σ),
-       own_bor κ (● to_gmap (1%Qp, DecAgree Bor_in) B) ∗
+       own_bor κ (● to_gmap (1%Qp, to_agree Bor_in) B) ∗
        box borN (to_gmap false B) Pb)%I.
 
    Definition lft_inh (κ : lft) (s : bool) (Pi : iProp Σ) : iProp Σ :=
@@ -171,7 +173,7 @@ Section defs.
   Definition bor_idx := (lft * slice_name)%type.
 
   Definition idx_bor_own (q : frac) (i : bor_idx) : iProp Σ :=
-    own_bor (i.1) (â—¯ {[ i.2 := (q,DecAgree Bor_in) ]}).
+    own_bor (i.1) (â—¯ {[ i.2 := (q, to_agree Bor_in) ]}).
   Definition idx_bor (κ : lft) (i : bor_idx) (P : iProp Σ) : iProp Σ :=
     (lft_incl κ (i.1) ∗ slice borN (i.2) P)%I.
   Definition raw_bor (κ : lft) (P : iProp Σ) : iProp Σ :=
@@ -254,6 +256,13 @@ Lemma lft_vs_unfold κ Pb Pi :
       lft_vs_inv κ I ∗ ▷ Pi ∗ own_cnt κ (◯ n).
 Proof. done. Qed.
 
+Global Instance own_bor_proper κ : Proper ((≡) ==> (≡)) (own_bor κ).
+Proof. solve_proper. Qed.
+Global Instance own_cnt_proper κ : Proper ((≡) ==> (≡)) (own_cnt κ).
+Proof. solve_proper. Qed.
+Global Instance own_inh_proper κ : Proper ((≡) ==> (≡)) (own_inh κ).
+Proof. solve_proper. Qed.
+
 Global Instance lft_bor_alive_ne κ n : Proper (dist n ==> dist n) (lft_bor_alive κ).
 Proof. solve_proper. Qed.
 Global Instance lft_bor_alive_proper κ : Proper ((≡) ==> (≡)) (lft_bor_alive κ).
diff --git a/theories/lifetime/faking.v b/theories/lifetime/faking.v
index 59e53e3cb4cde7a7c12487bc0448ba263dec8c5e..7ee7bd10c7a57a2da837c76b5b28dbb6f0db8d0e 100644
--- a/theories/lifetime/faking.v
+++ b/theories/lifetime/faking.v
@@ -1,5 +1,5 @@
 From lrust.lifetime Require Export primitive.
-From iris.algebra Require Import csum auth frac gmap dec_agree gset.
+From iris.algebra Require Import csum auth frac gmap agree gset.
 From iris.base_logic Require Import big_op.
 From iris.base_logic.lib Require Import boxes.
 From iris.proofmode Require Import tactics.
@@ -18,14 +18,14 @@ Proof.
   { iModIntro. iExists A, I. by iFrame. }
   iMod (own_alloc (● 0 ⋅ ◯ 0)) as (γcnt) "[Hcnt Hcnt']"; first done.
   iMod (own_alloc ((● ∅ ⋅ ◯ ∅) :auth (gmap slice_name
-      (frac * dec_agree bor_state)))) as (γbor) "[Hbor Hbor']";
+      (frac * agree bor_stateC)))) as (γbor) "[Hbor Hbor']";
     first by apply auth_valid_discrete_2.
   iMod (own_alloc ((● ∅) :auth (gset_disj slice_name)))
      as (γinh) "Hinh"; first by done.
   set (γs := LftNames γbor γcnt γinh).
   iMod (own_update with "HI") as "[HI Hγs]".
   { apply auth_update_alloc,
-      (alloc_singleton_local_update _ κ (DecAgree γs)); last done.
+      (alloc_singleton_local_update _ κ (to_agree γs)); last done.
     by rewrite lookup_fmap HIκ. }
   iDestruct "Hγs" as "#Hγs".
   iAssert (own_cnt κ (● 0)) with "[Hcnt]" as "Hcnt".
@@ -85,7 +85,7 @@ Proof.
   iMod (slice_insert_empty _ _ _ _ P with "Hbox") as (γ) "(% & #Hslice & Hbox)".
   iMod (own_bor_update with "HB●") as "[HB● H◯]".
   { eapply auth_update_alloc,
-      (alloc_singleton_local_update _ _ (1%Qp, DecAgree Bor_in)); last done.
+      (alloc_singleton_local_update _ _ (1%Qp, to_agree Bor_in)); last done.
     by do 2 eapply lookup_to_gmap_None. }
   rewrite /bor /raw_bor /idx_bor_own /=. iModIntro. iSplitR "Hâ—¯".
   - iExists ({[γ]} ∪ B), (P ∗ Pinh)%I. rewrite !to_gmap_union_singleton. by iFrame.
diff --git a/theories/lifetime/primitive.v b/theories/lifetime/primitive.v
index a47a04ee2917dfe069316e41428bbeb46f23e0bb..984f3d09208a883a2ad0a8323ce3c7ddc25b5115 100644
--- a/theories/lifetime/primitive.v
+++ b/theories/lifetime/primitive.v
@@ -1,5 +1,5 @@
 From lrust.lifetime Require Export definitions.
-From iris.algebra Require Import csum auth frac gmap dec_agree gset.
+From iris.algebra Require Import csum auth frac gmap agree gset.
 From iris.base_logic Require Import big_op.
 From iris.base_logic.lib Require Import boxes fractional.
 From iris.proofmode Require Import tactics.
@@ -10,21 +10,22 @@ Context `{invG Σ, lftG Σ}.
 Implicit Types κ : lft.
 
 Lemma to_borUR_included (B : gmap slice_name bor_state) i s q :
-  {[i := (q%Qp, DecAgree s)]} ≼ to_borUR B → B !! i = Some s.
+  {[i := (q%Qp, to_agree s)]} ≼ to_borUR B → B !! i = Some s.
 Proof.
-  rewrite singleton_included=> -[qs [/leibniz_equiv_iff]].
-  rewrite lookup_fmap fmap_Some=> -[s' [? ->]].
-  by move=> /Some_pair_included [_] /Some_included_total /DecAgree_included=>->.
+  rewrite singleton_included=> -[qs []]. unfold_leibniz.
+  rewrite lookup_fmap fmap_Some_equiv=> -[s' [-> ->]].
+  by move=> /Some_pair_included [_] /Some_included_total /to_agree_included=>->.
 Qed.
 
 (** Ownership *)
 Lemma own_ilft_auth_agree (I : gmap lft lft_names) κ γs :
   own_ilft_auth I -∗
-    own ilft_name (◯ {[κ := DecAgree γs]}) -∗ ⌜is_Some (I !! κ)⌝.
+    own ilft_name (◯ {[κ := to_agree γs]}) -∗ ⌜is_Some (I !! κ)⌝.
 Proof.
   iIntros "HI Hκ". iDestruct (own_valid_2 with "HI Hκ")
-    as %[[? [??]]%singleton_included _]%auth_valid_discrete_2.
-  unfold to_ilftUR in *. simplify_map_eq; simplify_option_eq; eauto.
+    as %[[? [Hl ?]]%singleton_included _]%auth_valid_discrete_2.
+  unfold to_ilftUR in *. simplify_map_eq.
+  destruct (fmap_Some_equiv' _ _ _ Hl) as (?&?&?). eauto.
 Qed.
 
 Lemma own_alft_auth_agree (A : gmap atomic_lft bool) Λ b :
@@ -50,13 +51,13 @@ Proof.
   iIntros "[Hx Hy]".
   iDestruct "Hx" as (γs) "[Hγs Hx]"; iDestruct "Hy" as (γs') "[Hγs' Hy]".
   iDestruct (own_valid_2 with "Hγs Hγs'") as %Hγs%auth_own_valid.
-  move: Hγs; rewrite /= op_singleton singleton_valid=> /dec_agree_op_inv [<-].
+  move: Hγs; rewrite /= op_singleton singleton_valid=> /agree_op_inv /(inj to_agree) [<-].
   iExists γs. iSplit. done. rewrite own_op; iFrame.
 Qed.
 Global Instance own_bor_into_op κ x x1 x2 :
   IntoOp x x1 x2 → IntoAnd false (own_bor κ x) (own_bor κ x1) (own_bor κ x2).
 Proof.
-  rewrite /IntoOp /IntoAnd=> /leibniz_equiv_iff->. by rewrite -own_bor_op.
+  rewrite /IntoOp /IntoAnd=>->. by rewrite -own_bor_op.
 Qed.
 Lemma own_bor_valid κ x : own_bor κ x -∗ ✓ x.
 Proof. iDestruct 1 as (γs) "[#? Hx]". by iApply own_valid. Qed.
@@ -84,7 +85,7 @@ Proof.
   iIntros "[Hx Hy]".
   iDestruct "Hx" as (γs) "[Hγs Hx]"; iDestruct "Hy" as (γs') "[Hγs' Hy]".
   iDestruct (own_valid_2 with "Hγs Hγs'") as %Hγs%auth_own_valid.
-  move: Hγs; rewrite /= op_singleton singleton_valid=> /dec_agree_op_inv [<-].
+  move: Hγs; rewrite /= op_singleton singleton_valid=> /agree_op_inv /(inj to_agree) [<-].
   iExists γs. iSplit; first done. rewrite own_op; iFrame.
 Qed.
 Global Instance own_cnt_into_op κ x x1 x2 :
@@ -118,7 +119,7 @@ Proof.
   iIntros "[Hx Hy]".
   iDestruct "Hx" as (γs) "[Hγs Hx]"; iDestruct "Hy" as (γs') "[Hγs' Hy]".
   iDestruct (own_valid_2 with "Hγs Hγs'") as %Hγs%auth_own_valid.
-  move: Hγs; rewrite /= op_singleton singleton_valid=> /dec_agree_op_inv [<-].
+  move: Hγs; rewrite /= op_singleton singleton_valid=> /agree_op_inv /(inj to_agree) [<-].
   iExists γs. iSplit. done. rewrite own_op; iFrame.
 Qed.
 Global Instance own_inh_into_op κ x x1 x2 :
@@ -281,7 +282,7 @@ Proof. done. Qed.
 Global Instance idx_bor_own_fractional i : Fractional (λ q, idx_bor_own q i)%I.
 Proof.
   intros p q. rewrite /idx_bor_own -own_bor_op /own_bor. f_equiv=>?.
-  by rewrite -auth_frag_op op_singleton.
+  rewrite -auth_frag_op op_singleton pair_op agree_idemp. done.
 Qed.
 Global Instance idx_bor_own_as_fractional i q :
   AsFractional (idx_bor_own q i) (λ q, idx_bor_own q i)%I q.
diff --git a/theories/lifetime/raw_reborrow.v b/theories/lifetime/raw_reborrow.v
index 2d122a2e4c463adb6bcbddb66b0dcb9906fb88d6..cde623f055df681dbd7a3117a9df0a4d5690b74e 100644
--- a/theories/lifetime/raw_reborrow.v
+++ b/theories/lifetime/raw_reborrow.v
@@ -1,6 +1,6 @@
 From lrust.lifetime Require Export primitive.
 From lrust.lifetime Require Import faking.
-From iris.algebra Require Import csum auth frac gmap dec_agree gset.
+From iris.algebra Require Import csum auth frac gmap agree gset.
 From iris.base_logic Require Import big_op.
 From iris.base_logic.lib Require Import boxes.
 From iris.proofmode Require Import tactics.
@@ -39,8 +39,9 @@ Proof.
   iMod (slice_empty with "Hislice Hbox") as "[HP Hbox]"; first done.
   { by rewrite lookup_fmap HB. }
   iMod (own_bor_update_2 with "HB● Hi") as "[HB● Hi]".
-  { eapply auth_update, singleton_local_update,
-     (exclusive_local_update _ (1%Qp, DecAgree (Bor_rebor κ'))); last done.
+  { eapply auth_update. (* FIXME: eapply singleton_local_update loops. *)
+    apply: singleton_local_update; last eapply
+     (exclusive_local_update _ (1%Qp, to_agree (Bor_rebor κ'))); last done.
     rewrite /to_borUR lookup_fmap. by rewrite HB. }
   iAssert (▷?q lft_inv A κ)%I with "[H◯ HB● HB Hvs' Hinh' Hbox]" as "Hκ".
   { iNext. rewrite /lft_inv. iLeft.
@@ -58,7 +59,7 @@ Proof.
   iDestruct "HBj" as %HBj; move: HBj; rewrite lookup_fmap fmap_None=> HBj.
   iMod (own_bor_update with "HB●") as "[HB● Hj]".
   { apply auth_update_alloc,
-     (alloc_singleton_local_update _ j (1%Qp, DecAgree Bor_in)); last done.
+     (alloc_singleton_local_update _ j (1%Qp, to_agree Bor_in)); last done.
     rewrite /to_borUR lookup_fmap. by rewrite HBj. }
   iModIntro. iExists (P ∗ Pb)%I. rewrite /Iinv. iFrame "HI". iFrame.
   iSplitL "Hj".
@@ -80,7 +81,7 @@ Proof.
     as %[HB%to_borUR_included _]%auth_valid_discrete_2.
   iMod (own_bor_update_2 with "HB● Hi") as "[HB● Hi]".
   { eapply auth_update, singleton_local_update,
-     (exclusive_local_update _ (1%Qp, DecAgree Bor_in)); last done.
+     (exclusive_local_update _ (1%Qp, to_agree Bor_in)); last done.
     rewrite /to_borUR lookup_fmap. by rewrite HB. }
   iMod (slice_fill _ _ false with "Hislice HP Hbox")
      as "Hbox"; first by solve_ndisj.
diff --git a/theories/lifetime/reborrow.v b/theories/lifetime/reborrow.v
index 2f6aafb4279ab09599bac3aefdf4689e4ff7e969..b899064431bdbd8ea3ebe8967bf0020b8a9537e8 100644
--- a/theories/lifetime/reborrow.v
+++ b/theories/lifetime/reborrow.v
@@ -1,6 +1,6 @@
 From lrust.lifetime Require Export borrow derived.
 From lrust.lifetime Require Import raw_reborrow accessors.
-From iris.algebra Require Import csum auth frac gmap dec_agree gset.
+From iris.algebra Require Import csum auth frac gmap agree gset.
 From iris.base_logic Require Import big_op.
 From iris.base_logic.lib Require Import boxes.
 From iris.proofmode Require Import tactics.
@@ -75,7 +75,7 @@ Proof.
     - rewrite big_sepM_delete; last done. iDestruct "HB" as "[_ $]". }
   iMod (raw_bor_unnest' _ false with "[$HI $Hinv] HP Halive [Hvs]") as (Pb'') "([HI Hinv] & HP & Halive & Hvs)";
     [solve_ndisj|exact: gmultiset_union_subseteq_l|done| |].
-  { (* TODO: Use iRewrite supporting cotnractive rewriting. *)
+  { (* TODO: Use iRewrite supporting contractive rewriting. *)
     iApply (lft_vs_cons with "[]"); last done.
      iIntros "[$ Hbor]". iModIntro. iNext. by iRewrite "EQ". }
   iMod ("Hclose" with "[-HP]") as "_".
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index fa7968718a8a3edfded14d66e971ef931d3786c0..4bfb93ffbdbd5164b3bce169421ae66ccb5af122 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -156,4 +156,4 @@ Section incl.
       iMod (Hincl with "LFT Hρ") as "#Hincl". iIntros "!>!#*H". iSplit; last done.
       iDestruct "H" as (i) "[??]". iExists _. iSplit. done. by iApply "Hincl".
   Qed.
-End incl.
\ No newline at end of file
+End incl.