diff --git a/opam.pins b/opam.pins
index e9084293d608a87962aafe48434881bc8c09f431..0af3bc663e38f5b207a1047905a788bb36a89f18 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 21fbbdde77c9e8b5d9cf2ad908c0921528ca02f2
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 5874f41e10c229d0b7df07a1e4e58f5e61a1af0a
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 2182ff1acf7633b0d9af062e075a0d14a127ad1d..8750b714cb43629b8e70b75fbc76e7ef331006f4 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -55,7 +55,7 @@ Section fn.
             type_dist2 n') fn.
   Proof.
     intros fp1 fp2 Hfp. apply ty_of_st_type_ne. destruct n'; first done.
-    constructor; simpl.
+    constructor; unfold ty_own; simpl.
     (* TODO: 'f_equiv' is slow here because reflexivity is slow. *)
     (* The clean way to do this would be to have a metric on type contexts. Oh well. *)
     intros tid vl. unfold typed_body.
diff --git a/theories/typing/lib/cell.v b/theories/typing/lib/cell.v
index 6a729cc5d8bd9c65e5d1884d7ab78e39cbc55f87..f67534e7e6101ed0ae91bf5637fd2f7fe936affb 100644
--- a/theories/typing/lib/cell.v
+++ b/theories/typing/lib/cell.v
@@ -49,7 +49,7 @@ Section cell.
   Global Instance cell_copy :
     Copy ty → Copy (cell ty).
   Proof.
-    intros ty Hcopy. split; first by intros; simpl; apply _.
+    intros ty Hcopy. split; first by intros; simpl; unfold ty_own; apply _.
     iIntros (κ tid E F l q ??) "#LFT #Hshr Htl Htok". iExists 1%Qp. simpl in *.
     (* Size 0 needs a special case as we can't keep the thread-local invariant open. *)
     destruct (ty_size ty) as [|sz] eqn:Hsz; simpl in *.
diff --git a/theories/typing/lib/rc.v b/theories/typing/lib/rc.v
index f6b8962ffc48b4ec230a6156de319643775dd734..b0cb325a52a32f269254370fd1dfb214c10c67b8 100644
--- a/theories/typing/lib/rc.v
+++ b/theories/typing/lib/rc.v
@@ -1,3 +1,4 @@
+From Coq.QArith Require Import Qcanon.
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import auth csum frac agree.
 From iris.base_logic Require Import big_op.
@@ -45,10 +46,10 @@ Section rc.
        ty_shr κ tid l :=
          ∃ (l' : loc), &frac{κ} (λ q, l↦∗{q} [ #l']) ∗
            □ ∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌝ -∗ q.[κ]
-             ={F, F∖↑shrN}▷=∗ q.[κ] ∗ ∃ γ ν q',
+             ={F, F∖↑shrN}▷=∗ q.[κ] ∗ ∃ γ ν q', κ ⊑ ν ∗
                 na_inv tid rc_invN (rc_inv tid ν γ l' ty) ∗
-                &na{κ, tid, rc_invN}(own γ (◯ Some (q', 1%positive))) ∗
-                ty.(ty_shr) κ tid (shift_loc l' 1)
+                &na{κ, tid, rc_shrN}(own γ (◯ Some (q', 1%positive))) ∗
+                ty.(ty_shr) ν tid (shift_loc l' 1)
     |}%I.
   Next Obligation. by iIntros (ty tid [|[[]|][]]) "H". Qed.
   Next Obligation.
@@ -60,10 +61,10 @@ Section rc.
       try by iMod (bor_persistent_tok with "LFT Hb Htok") as "[>[] _]".
     iFrame "Htok". iExists _. iFrame "#". rewrite bor_unfold_idx.
     iDestruct "Hb" as (i) "(#Hpb&Hpbown)".
-    set (C := (∃ _ _ _, _ ∗ &na{_,_,_} _ ∗ _)%I).
+    set (C := (∃ _ _ _, _ ∗ _ ∗ &na{_,_,_} _ ∗ _)%I).
     iMod (inv_alloc shrN _ (idx_bor_own 1 i ∨ C)%I
           with "[Hpbown]") as "#Hinv"; first by iLeft.
-    iIntros "!> !# * % Htok". iMod (inv_open with "Hinv") as "[INV Hclose]"; first set_solver.
+    iIntros "!> !# * % Htok". iMod (inv_open with "Hinv") as "[INV Hclose1]"; first set_solver.
     iDestruct "INV" as "[>Hbtok|#Hshr]".
     - iAssert (&{κ} _)%I with "[Hbtok]" as "Hb".
       { rewrite bor_unfold_idx. iExists _. by iFrame. }
@@ -98,10 +99,10 @@ Section rc.
         iDestruct (frac_bor_lft_incl with "LFT >[Hlft]") as "#Hlft".
         { iApply (bor_fracture with "LFT"); first solve_ndisj. by rewrite Qp_mult_1_r. }
         iMod (bor_na with "Hrc") as "$"; first solve_ndisj.
-        iApply ty_shr_mono; done. }
-      iMod ("Hclose" with "[]") as "_"; first by auto.
+        by iFrame "#". }
+      iMod ("Hclose1" with "[]") as "_"; first by auto.
       by iFrame "#∗".
-    - iMod ("Hclose" with "[]") as "_"; first by auto.
+    - iMod ("Hclose1" with "[]") as "_"; first by auto.
       iApply step_fupd_intro; first solve_ndisj. iNext. by iFrame.
   Qed.
   Next Obligation.
@@ -111,10 +112,10 @@ Section rc.
     iMod (lft_incl_acc with "Hincl Htok") as (q'') "[Htok Hclose]"; first solve_ndisj.
     iMod ("Hshr" with "[] Htok") as "Hshr2"; first done.
     iModIntro. iNext. iMod "Hshr2" as "[Htok HX]".
-    iMod ("Hclose" with "Htok") as "$". iDestruct "HX" as (???) "(? & ? & ?)".
+    iMod ("Hclose" with "Htok") as "$". iDestruct "HX" as (? ν ?) "(? & ? & ?& ?)".
     iExists _, _, _. iModIntro. iFrame. iSplit.
+    - by iApply lft_incl_trans.
     - by iApply na_bor_shorten.
-    - by iApply ty_shr_mono.
   Qed.
 End rc.
 
@@ -137,7 +138,7 @@ Section code.
       iIntros (_ ret arg). inv_vec arg=>x. simpl_subst.
     iApply type_new; [solve_typing..|]; iIntros (rcbox); simpl_subst.
     iApply type_new; [solve_typing..|]; iIntros (rc); simpl_subst.
-    iIntros (tid qE) "#LFT Hna HE HL Hk HT". simpl_subst.
+    iIntros (tid qE) "#LFT Hna HE HL Hk HT".
     rewrite (Nat2Z.id (S ty.(ty_size))) 2!tctx_interp_cons
             tctx_interp_singleton !tctx_hasty_val.
     iDestruct "HT" as "[Hrc [Hrcbox Hx]]". destruct x as [[|lx|]|]; try done.
@@ -164,4 +165,69 @@ Section code.
     iApply type_delete; [solve_typing..|].
     iApply (type_jump [ #_]); solve_typing.
   Qed.
+
+  Definition rc_clone : val :=
+    funrec: <> ["rc"] :=
+      let: "rc2" := new [ #1 ] in
+      let: "rc'" := !"rc" in
+      let: "rc''" := !"rc'" in
+      let: "count" := !("rc''" +ₗ #0) in
+      "rc''" +ₗ #0 <- "count" +#1;;
+      "rc2" <- "rc''";;
+      delete [ #1; "rc" ];; return: ["rc2"].
+
+  Lemma rc_clone_type ty :
+    typed_val rc_clone (fn(∀ α, [α]; &shr{α} rc ty) → rc ty).
+  Proof.
+    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros (α ret arg). inv_vec arg=>x. simpl_subst.
+    iApply type_new; [solve_typing..|]; iIntros (rc2); simpl_subst.
+    rewrite (Nat2Z.id 1). (* Having to do this is rather annoying... *) 
+    iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
+    iIntros (tid qE) "#LFT Hna HE HL Hk".
+    rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
+    iIntros "[Hx [Hrc' Hrc2]]". rewrite [[x]]lock.
+    destruct rc' as [[|lrc|]|]; try done. iDestruct "Hrc'" as (l') "[#Hlrc #Hshr]".
+    destruct rc2 as [[|lrc2|]|]; try done. iDestruct "Hrc2" as "[Hrc2 Hrc2†]".
+    iDestruct "Hrc2" as (vl) "Hrc2". rewrite uninit_own.
+    iDestruct "Hrc2" as "[>Hrc2↦ >SZ]". destruct vl as [|]; iDestruct "SZ" as %[=].
+    destruct vl as [|]; last done. rewrite heap_mapsto_vec_singleton.
+    (* All right, we are done preparing our context. Let's get going. *)
+    rewrite {1}/elctx_interp big_sepL_singleton.
+    iDestruct "HE" as "[Hα1 Hα2]". wp_bind (!_)%E.
+    iSpecialize ("Hshr" with "[] Hα1"); last iApply (wp_fupd_step with "Hshr"); [done..|].
+    iMod (frac_bor_acc with "LFT Hlrc Hα2") as (q') "[Hlrc↦ Hclose]"; first solve_ndisj.
+    rewrite heap_mapsto_vec_singleton. iApply wp_fupd. wp_read.
+    iMod ("Hclose" with "[$Hlrc↦]") as "Hα2". iIntros "!> [Hα1 Hproto]".
+    iDestruct "Hproto" as (γ ν q'') "(#Hincl & #Hinv & #Hrctokb & #Hshr)". iModIntro.
+    wp_let. wp_op. rewrite shift_loc_0.
+    (* Finally, finally... opening the thread-local Rc protocol. *)
+    iMod (na_inv_open with "Hinv Hna") as "(Hrcproto & Hna & Hclose1)"; [solve_ndisj..|].
+    iMod (na_bor_acc with "LFT Hrctokb Hα1 Hna") as "(>Hrctok & Hna & Hclose2)"; [solve_ndisj..|].
+    iDestruct "Hrcproto" as (st) "[>Hrc● Hrcst]".
+    iDestruct (own_valid_2 with "Hrc● Hrctok") as %[[Hval|[_ [[qa c] [_ [-> _]]]]]%option_included _]%auth_valid_discrete_2; first done. (* Oh my, what a pattern... *)
+    iDestruct "Hrcst" as (qb) "(>Hl' & >Hl'† & >% & Hνtok & Hν†)".
+    wp_read. wp_let. wp_op. rewrite shift_loc_0. wp_op. wp_write. wp_write.
+    (* And closing it again. *)
+    iMod (own_update with "Hrc●") as "[Hrc● Hrctok2]".
+    { apply auth_update_alloc,
+      (op_local_update_discrete _ _ (Some ((qb/2)%Qp, 1%positive)))=>-[/= Hqa _].
+      split; simpl; last done. apply frac_valid'. rewrite -H comm_L -{2}(Qp_div_2 qb).
+      apply Qcplus_le_mono_l. rewrite -{1}(Qcplus_0_l (_ / _)%Qp).
+      apply Qcplus_le_mono_r, Qp_ge_0. }
+    rewrite right_id -Some_op pair_op. iDestruct "Hνtok" as "[Hνtok1 Hνtok2]".
+    iMod ("Hclose2" with "[$Hrctok] Hna") as "[Hα1 Hna]".
+    iMod ("Hclose1" with "[Hrc● Hl' Hl'† Hνtok2 Hν† $Hna]") as "Hna".
+    { iExists _. iFrame "Hrc●". iExists _. rewrite Z.add_comm. iFrame.
+      iNext. iPureIntro. rewrite [_ ⋅ _]comm frac_op' -assoc Qp_div_2. done. }
+    (* Finish up the proof. *)
+    iApply (type_type _ _ _ [ x ◁ box (&shr{α} rc ty); #lrc2 ◁ box (rc ty)]%TC
+        with "[] LFT Hna [Hα1 Hα2] HL Hk [-]"); last first.
+    { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
+      unlock. iFrame "Hx". iFrame "Hrc2†". iExists _. erewrite heap_mapsto_vec_singleton.
+      iFrame "Hrc2↦". iNext. iRight. iExists _, ν, _. iFrame "#∗". }
+    { rewrite /elctx_interp big_sepL_singleton. iFrame. }
+    iApply type_delete; [solve_typing..|].
+    iApply (type_jump [ #_ ]); solve_typing.
+  Qed.
 End code.
diff --git a/theories/typing/lib/refcell/ref_code.v b/theories/typing/lib/refcell/ref_code.v
index a7ee9b1fb11e078302523803c4508d1c72cc2275..952f950eb315023aa8fb710a5a744f30671b767b 100644
--- a/theories/typing/lib/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -81,7 +81,7 @@ Section ref_functions.
          (op_local_update_discrete _ _ (reading_st (q''/2)%Qp ν))=>-[Hagv _].
       split; [|split; last done].
       - by rewrite /= agree_idemp.
-      - change ((q''/2+q')%Qp ≤ 1%Qp)%Qc. rewrite -Hq'q'' comm -{2}(Qp_div_2 q'').
+      - apply frac_valid'. rewrite -Hq'q'' comm -{2}(Qp_div_2 q'').
         apply Qcplus_le_mono_l. rewrite -{1}(Qcplus_0_l (q''/2)%Qp).
         apply Qcplus_le_mono_r, Qp_ge_0. }
     wp_apply wp_new; [done..|]. iIntros (lr ?) "(%&?&Hlr)".
diff --git a/theories/typing/lib/refcell/refcell_code.v b/theories/typing/lib/refcell/refcell_code.v
index c5b433be50458c4dd3fc08b5d6fe87ac83a6899d..93bb78de5f0458df6fdd87aa7638068a3cb2b1ec 100644
--- a/theories/typing/lib/refcell/refcell_code.v
+++ b/theories/typing/lib/refcell/refcell_code.v
@@ -42,7 +42,7 @@ Section refcell_functions.
     { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //=. iFrame.
       iSplitL "Hx↦".
       - iExists _. rewrite uninit_own. auto.
-      - iExists (_::_). rewrite heap_mapsto_vec_cons. iFrame. auto. }
+      - iExists (_::_). rewrite heap_mapsto_vec_cons. iFrame. simpl. iFrame. auto. }
     iApply type_delete; [solve_typing..|].
     iApply (type_jump [ #_]); solve_typing.
   Qed.
@@ -186,7 +186,7 @@ Section refcell_functions.
             (op_local_update_discrete _ _ (reading_st (q'/2)%Qp ν))=>-[Hagv _].
             split; [|split].
             - by rewrite /= -Hag agree_idemp.
-            - change ((q'/2+q)%Qp ≤ 1%Qp)%Qc. rewrite -Hqq' comm -{2}(Qp_div_2 q').
+            - apply frac_valid'. rewrite -Hqq' comm -{2}(Qp_div_2 q').
               apply Qcplus_le_mono_l. rewrite -{1}(Qcplus_0_l (q'/2)%Qp).
               apply Qcplus_le_mono_r, Qp_ge_0.
             - done. }
diff --git a/theories/typing/lib/refcell/refmut_code.v b/theories/typing/lib/refcell/refmut_code.v
index c5039c184e0e7c64a4f5e00d94ac84c0302cee1a..5602f7fbfc3ab0e13edda9ef770170afda91bb3f 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -210,7 +210,7 @@ Section refmut_functions.
       iDestruct "Href" as ([|[[|lv'|]|] [|]]) "[H↦ Href]"; auto.
       iExists [ #lv'; #lrc].
       rewrite (heap_mapsto_vec_cons _ _ _ [_]) !heap_mapsto_vec_singleton. iFrame.
-      iExists ν. rewrite EQ1. eauto 10 with iFrame. }
+      iExists ν. rewrite /= EQ1. eauto 20 with iFrame. }
     { rewrite /elctx_interp !big_sepL_cons /= -lft_tok_sep. iFrame. }
     iApply type_deref; [solve_typing..|]. iIntros (x'). simpl_subst.
     iApply type_deref; [solve_typing..|]. iIntros (f'). simpl_subst.
diff --git a/theories/typing/lib/rwlock/rwlock_code.v b/theories/typing/lib/rwlock/rwlock_code.v
index 18b83f2536ff2860e1058ce4eb206fe968bfe046..8a036dc71472104ce464a55040e9d98731fa29b5 100644
--- a/theories/typing/lib/rwlock/rwlock_code.v
+++ b/theories/typing/lib/rwlock/rwlock_code.v
@@ -42,7 +42,7 @@ Section rwlock_functions.
     { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //=. iFrame.
       iSplitL "Hx↦".
       - iExists _. rewrite uninit_own. auto.
-      - iExists (_::_). rewrite heap_mapsto_vec_cons. iFrame. auto. }
+      - iExists (_::_). rewrite heap_mapsto_vec_cons. iFrame. simpl. iFrame. auto. }
     iApply type_delete; [solve_typing..|].
     iApply (type_jump [ #_]); solve_typing.
   Qed.
@@ -193,7 +193,7 @@ Section rwlock_functions.
               (op_local_update_discrete _ _ (reading_st (q'/2)%Qp ν))=>-[Hagv _].
               split; [split|].
               - by rewrite /= Hag agree_idemp.
-              - change ((q'/2+q)%Qp ≤ 1%Qp)%Qc. rewrite -Hqq' comm -{2}(Qp_div_2 q').
+              - apply frac_valid'. rewrite -Hqq' comm -{2}(Qp_div_2 q').
                 apply Qcplus_le_mono_l. rewrite -{1}(Qcplus_0_l (q'/2)%Qp).
                 apply Qcplus_le_mono_r, Qp_ge_0.
               - done. }
diff --git a/theories/typing/product_split.v b/theories/typing/product_split.v
index 2d56f54e397b9103780ad3290c7e4e43a72e7ea0..47a6b6fa778ba783b97b5dfb891c3b27941a344d 100644
--- a/theories/typing/product_split.v
+++ b/theories/typing/product_split.v
@@ -116,7 +116,7 @@ Section product_split.
     iDestruct "H↦1" as (vl1) "[H↦1 H1]". iDestruct "H↦2" as (vl2) "[H↦2 H2]".
     iExists (vl1 ++ vl2). rewrite heap_mapsto_vec_app. iFrame.
     iDestruct (ty_size_eq with "H1") as "#>EQ". iDestruct "EQ" as %->.
-    auto 10 with iFrame.
+    rewrite {3}/ty_own /=. auto 10 with iFrame.
   Qed.
 
   Lemma tctx_split_own_prod E L n tyl p :
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index f36ed5ae8f33d44f1a3ce8550bc097ddb33ffc2c..9f53f4c187e1318dfa3385a90ff4cfeeb4aae12b 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -107,7 +107,7 @@ Section sum.
     { clear EQmax. induction EQ as [|???? EQ _ IH]=>-[|i] //=. }
     constructor; simpl.
     - by rewrite EQmax.
-    - intros tid vl. destruct n as [|n]=> //=. rewrite EQmax.
+    - intros tid vl. destruct n as [|n]=> //=. rewrite /ty_own /= EQmax.
       solve_proper_core ltac:(fun _ => exact:EQnth || f_type_equiv || f_equiv).
     - intros κ tid l. unfold is_pad. rewrite EQmax.
       solve_proper_core ltac:(fun _ => exact:EQnth || f_type_equiv || f_equiv).
@@ -125,7 +125,7 @@ Section sum.
     { clear EQmax. induction EQ as [|???? EQ _ IH]=>-[|i] //=. }
     constructor; simpl.
     - by rewrite EQmax.
-    - intros tid vl. rewrite EQmax.
+    - intros tid vl. rewrite /ty_own /= EQmax.
       solve_proper_core ltac:(fun _ => exact:EQnth || f_equiv).
     - intros κ tid l. unfold is_pad. rewrite EQmax.
       solve_proper_core ltac:(fun _ => exact:EQnth || (eapply ty_size_ne; try reflexivity) || f_equiv).
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 94219da468cbd76c1bc4984c64c4d18e5308c181..563a333eb62e4c55694870ec4165b34ec320aee7 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -51,6 +51,8 @@ Instance: Params (@ty_size) 2.
 Instance: Params (@ty_own) 2.
 Instance: Params (@ty_shr) 2.
 
+Arguments ty_own {_ _} !_ _ !_ /.
+
 Record simple_type `{typeG Σ} :=
   { st_own : thread_id → list val → iProp Σ;
     st_size_eq tid vl : st_own tid vl -∗ ⌜length vl = 1%nat⌝;
@@ -316,7 +318,7 @@ Section type_contractive.
   Proof.
     intros ???. constructor.
     - done.
-    - intros. destruct n; first done; simpl. by f_equiv.
+    - intros. destruct n; first done; simpl. f_equiv. f_equiv. done.
     - intros. solve_contractive.
   Qed.
 End type_contractive.
diff --git a/theories/typing/type_sum.v b/theories/typing/type_sum.v
index da864583303e6b2a5051866f3e994023a127b20d..2df653e81db8c502e83c2ad95c2cfd93a37c4c1e 100644
--- a/theories/typing/type_sum.v
+++ b/theories/typing/type_sum.v
@@ -41,7 +41,7 @@ Section case.
         iFrame. iExists _. iFrame. rewrite uninit_own. auto.
     - rewrite -EQlen app_length -(Nat.add_1_l (_+_)) -!freeable_sz_split. iFrame.
       iExists (#i :: vl' ++ vl''). iNext. rewrite heap_mapsto_vec_cons heap_mapsto_vec_app.
-      iFrame. iExists i, vl', vl''. rewrite /= app_length nth_lookup EQty. auto.
+      iFrame. iExists i, vl', vl''. rewrite /= -EQlen app_length nth_lookup EQty /=. auto.
   Qed.
 
   Lemma type_case_own E L C T T' p n tyl el :
@@ -91,7 +91,7 @@ Section case.
     - iMod ("Hclose'" with "[] [H↦i H↦vl' H↦vl'' Hown]") as "[Hb Htok]";
         [by iIntros "!>$"| |].
       { iExists (#i::vl'++vl'').
-        rewrite heap_mapsto_vec_cons heap_mapsto_vec_app -EQlen. iFrame. iNext.
+        rewrite heap_mapsto_vec_cons heap_mapsto_vec_app /= -EQlen. iFrame. iNext.
         iExists i, vl', vl''. rewrite nth_lookup EQty. auto. }
       iMod ("Hclose" with "Htok") as "[HE HL]".
       iApply (Hety with "LFT Hna HE HL HC").