diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index 1bed6feaeb33d65a9808eaaee08fb16da71ed23a..4a48c547a57cbd3e0bc28c034ea103fcd72116ab 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -55,7 +55,10 @@ Section rc.
   Definition rc_persist tid ν (γ : gname) (l : loc) (ty : type) : iProp Σ :=
     (∃ ty', ▷ type_incl ty' ty ∗
               na_inv tid rc_invN (rc_inv tid ν γ l ty') ∗
-              ty.(ty_shr) ν tid (shift_loc l 2) ∗
+              (* 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) ν tid (shift_loc l 2) ∨ [†ν]) ∗
               □ (1.[ν] ={↑lftN,∅}▷=∗ [†ν]))%I.
 
   Global Instance rc_persist_ne ν γ l n :
@@ -68,10 +71,11 @@ Section rc.
   Lemma rc_persist_type_incl tid ν γ l ty1 ty2:
     type_incl ty1 ty2 -∗ rc_persist tid ν γ l ty1 -∗ rc_persist tid ν γ l ty2.
   Proof.
-    iIntros "#Hincl H". iDestruct "H" as (ty) "#(?&?&?&?)". iExists ty.
+    iIntros "#Hincl H". iDestruct "H" as (ty) "#(?&?& Hs &?)". iExists ty.
     iFrame "#". iSplit.
     - iNext. by iApply type_incl_trans.
-    - iDestruct "Hincl" as "(_&_&Hincls)". by iApply "Hincls".
+    - iDestruct "Hs" as "[?|?]"; last auto.
+      iLeft. iDestruct "Hincl" as "(_&_&Hincls)". by iApply "Hincls".
   Qed.
 
   Program Definition rc (ty : type) :=
@@ -134,7 +138,8 @@ Section rc.
         { rewrite /rc_inv. iExists (Some $ Cinl (_, _), _). iFrame. iExists _.
           iFrame "#∗". rewrite Qp_div_2; auto. }
         iMod (ty_share with "LFT HP Hν1") as "[??]"; first solve_ndisj.
-        iExists _, _, _. iFrame. iExists ty. iFrame "#". by iApply type_incl_refl. }
+        iExists _, _, _. iFrame. iExists ty. iFrame "#". iSplitR; last by auto.
+          by iApply type_incl_refl. }
       iDestruct "HX" as (γ ν q') "(#Hpersist & Hrctok)".
       iMod ("Hclose2" with "[] Hrctok") as "[HX $]"; first by (unfold X; auto 10).
       iAssert C with "[>HX]" as "#$".
@@ -327,7 +332,7 @@ Section code.
       "rcbox" +ₗ #0 <- #1;;
       "rcbox" +ₗ #1 <- #1;;
       "rcbox" +ₗ #2 <-{ty.(ty_size)} !"x";;
-      "rc" +ₗ #0 <- "rcbox";;
+      "rc" <- "rcbox";;
       delete [ #ty.(ty_size); "x"];; return: ["rc"].
 
   Lemma rc_new_type ty `{!TyWf ty} :
@@ -458,7 +463,9 @@ Section code.
     iApply wp_fupd. wp_read.
     iMod ("Hclose2" with "[$Hrc'↦]") as "Hα2". iIntros "!> [Hα1 #Hproto] !>".
     iDestruct "Hproto" as (γ ν q'') "#(Hαν & Hpersist & _)".
-    iDestruct "Hpersist" as (ty') "(_ & _ & Hshr & _)".
+    iDestruct "Hpersist" as (ty') "(_ & _ & [Hshr|Hν†] & _)"; last first.
+    { iMod (lft_incl_dead with "Hαν Hν†") as "Hα†". done.
+      iDestruct (lft_tok_dead with "Hα1 Hα†") as "[]". }
     wp_op. wp_write. iMod ("Hclose1" with "[$Hα1 $Hα2] HL") as "HL".
     (* Finish up the proof. *)
     iApply (type_type _ _ _ [ rcx ◁ box (&shr{α} rc ty); #lrc2 ◁ box (&shr{α} ty)]
diff --git a/theories/typing/lib/rc/weak.v b/theories/typing/lib/rc/weak.v
index ceebc7096659cbea1fadc53acd3c741df45d4f95..35e2364825e0cc09fd93bf29be9665ef279b3914 100644
--- a/theories/typing/lib/rc/weak.v
+++ b/theories/typing/lib/rc/weak.v
@@ -441,4 +441,47 @@ Section code.
       { unlock. by rewrite tctx_interp_singleton tctx_hasty_val. }
       iApply type_jump; solve_typing.
   Qed.
+
+  Definition weak_new ty : val :=
+    funrec: <> [] :=
+      let: "rcbox" := new [ #(2 + ty.(ty_size))%nat ] in
+      let: "w" := new [ #1 ] in
+      "rcbox" +ₗ #0 <- #0;;
+      "rcbox" +ₗ #1 <- #1;;
+      "w" <- "rcbox";;
+      return: ["w"].
+
+  Lemma weak_new_type ty `{!TyWf ty} :
+    typed_val (weak_new ty) (fn(∅) → weak ty).
+  Proof.
+    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros (_ ϝ ret arg). inv_vec arg. simpl_subst.
+    iApply type_new; [solve_typing..|]; iIntros (rcbox); simpl_subst.
+    iApply type_new; [solve_typing..|]; iIntros (w); simpl_subst.
+    iIntros (tid) "#LFT #HE Hna HL Hk [Hw [Hrcbox _]]".
+    rewrite (Nat2Z.id (2 + ty.(ty_size))) !tctx_hasty_val.
+    iDestruct (ownptr_uninit_own with "Hrcbox") as (lrcbox vlrcbox)
+       "(% & Hrcbox↦ & Hrcbox†)". subst rcbox. inv_vec vlrcbox=>??? /=.
+    iDestruct (heap_mapsto_vec_cons with "Hrcbox↦") as "[Hrcbox↦0 Hrcbox↦1]".
+    iDestruct (heap_mapsto_vec_cons with "Hrcbox↦1") as "[Hrcbox↦1 Hrcbox↦2]".
+    iDestruct (ownptr_uninit_own with "Hw") as (lw vlw) "(% & Hw↦ & Hw†)". subst w.
+    inv_vec vlw=>?. rewrite heap_mapsto_vec_singleton.
+    (* All right, we are done preparing our context. Let's get going. *)
+    wp_op. rewrite shift_loc_0. wp_write. wp_op. wp_write.
+    iMod (lft_create with "LFT") as (ν) "[Hν #Hν†]"; first done.
+    iPoseProof ("Hν†" with "Hν") as "H†". wp_bind (_ <- _)%E.
+    iApply wp_mask_mono; last iApply (wp_step_fupd with "H†"); [solve_ndisj..|].
+    wp_write. iIntros "#Hν !>". wp_seq.
+    iApply (type_type _ _ _ [ #lw ◁ box (weak ty)]
+        with "[] LFT HE Hna HL Hk [> -]"); last first.
+    { rewrite tctx_interp_singleton tctx_hasty_val' //=. iFrame.
+      iExists [_]. rewrite heap_mapsto_vec_singleton. iFrame.
+      iMod (own_alloc (● _ ⋅ ◯ _)) as (γ) "[??]"; last (iExists _, _; iFrame).
+      { apply auth_valid_discrete_2. by split. }
+      iExists ty. iFrame "Hν†". iSplitR; first by iApply type_incl_refl.
+      iSplitL; last by iRight. iMod (na_inv_alloc with "[-]") as "$"; last done.
+      iExists _. iFrame. rewrite freeable_sz_full_S shift_loc_assoc. iFrame.
+      iExists _. iFrame. rewrite vec_to_list_length. auto. }
+    iApply type_jump; solve_typing.
+  Qed.
 End code.