diff --git a/theories/typing/lib/rc.v b/theories/typing/lib/rc.v
index 1066f66d7f926084582104ea9a49e7ccd72666ae..1716a975415911148be4026563be28add86470da 100644
--- a/theories/typing/lib/rc.v
+++ b/theories/typing/lib/rc.v
@@ -119,3 +119,51 @@ Section rc.
     - by iApply ty_shr_mono.
   Qed.
 End rc.
+
+Section code.
+  Context `{!typeG Σ, !rcG Σ}.
+
+  Definition rc_new ty : val :=
+    funrec: <> ["x"] :=
+      let: "rcbox" := new [ #(S ty.(ty_size))] in
+      let: "rc" := new [ #1 ] in
+      "rcbox" +â‚— #0 <- #1;;
+      "rcbox" +â‚— #1 <-{ty.(ty_size)} !"x";;
+      "rc" +â‚— #0 <- "rcbox";;
+      delete [ #ty.(ty_size) ; "x"];; "return" ["rc"].
+
+  Lemma rc_new_type ty :
+    typed_val (rc_new ty) (fn([]; 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 (rcbox); simpl_subst.
+    iApply type_new; [solve_typing..|]; iIntros (rc); simpl_subst.
+    iIntros (tid qE) "#LFT Hna HE HL Hk HT". simpl_subst.
+    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.
+    iDestruct "Hx" as "[Hx Hx†]". iDestruct "Hx" as (vl) "[Hx↦ Hx]".
+    destruct rcbox as [[|lrcbox|]|]; try done. iDestruct "Hrcbox" as "[Hrcbox Hrcbox†]".
+    iDestruct "Hrcbox" as (vl') "Hrcbox". rewrite uninit_own.
+    iDestruct "Hrcbox" as "[>Hrcbox↦ >SZ]". destruct vl' as [|]; iDestruct "SZ" as %[=].
+    rewrite heap_mapsto_vec_cons. iDestruct "Hrcbox↦" as "[Hrcbox↦0 Hrcbox↦1]".
+    destruct rc as [[|lrc|]|]; try done. iDestruct "Hrc" as "[Hrc Hrc†]".
+    iDestruct "Hrc" as (vl'') "Hrc". rewrite uninit_own.
+    iDestruct "Hrc" as "[>Hrc↦ >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. *)
+    wp_op. rewrite shift_loc_0. wp_write. wp_op. iDestruct (ty.(ty_size_eq) with "Hx") as %Hsz.
+    wp_apply (wp_memcpy with "[$Hrcbox↦1 $Hx↦]"); [done||lia..|].
+    iIntros "[Hrcbox↦1 Hx↦]". wp_seq. wp_op. rewrite shift_loc_0. wp_write.
+    iApply (type_type _ _ _ [ #lx ◁ box (uninit (ty_size ty)); #lrc ◁ box (rc ty)]%TC
+        with "[] LFT Hna HE HL Hk [-]"); last first.
+    { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //=. iFrame.
+      iSplitL "Hx↦".
+      { iExists _. rewrite uninit_own. auto. }
+      iNext. iExists [_]. rewrite heap_mapsto_vec_singleton. iFrame. iFrame. iLeft.
+      rewrite freeable_sz_full_S. iFrame. iExists _. iFrame.  }
+    iApply type_delete; [solve_typing..|].
+    iApply (type_jump [ #_]); solve_typing.
+  Qed.
+End code.
diff --git a/theories/typing/lib/refcell/refcell_code.v b/theories/typing/lib/refcell/refcell_code.v
index f5e4931519f6d41333b7e0cb38a90c9037609a92..91f67707ed9ce0c4aa9c1f4519adc08da4d9b767 100644
--- a/theories/typing/lib/refcell/refcell_code.v
+++ b/theories/typing/lib/refcell/refcell_code.v
@@ -17,7 +17,7 @@ Section refcell_functions.
       let: "r" := new [ #(S ty.(ty_size))] in
       "r" +â‚— #0 <- #0;;
       "r" +â‚— #1 <-{ty.(ty_size)} !"x";;
-       delete [ #ty.(ty_size) ; "x"];; "return" ["r"].
+      delete [ #ty.(ty_size) ; "x"];; "return" ["r"].
 
   Lemma refcell_new_type ty :
     typed_val (refcell_new ty) (fn([]; ty) → refcell ty).
diff --git a/theories/typing/own.v b/theories/typing/own.v
index 91060a0badd421d9620af802569bb21d401c6c73..b1019731842c3d8c50dd2a2f0b49974b2aed5dea 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -21,7 +21,7 @@ Section own.
   Global Instance freable_sz_timeless n sz l : TimelessP (freeable_sz n sz l).
   Proof. destruct sz, n; apply _. Qed.
 
-  Lemma freeable_sz_full n l : freeable_sz n n l ⊣⊢ (†{1}l…n ∨ ⌜Z.of_nat n = 0⌝)%I.
+  Lemma freeable_sz_full n l : freeable_sz n n l ⊣⊢ †{1}l…n ∨ ⌜Z.of_nat n = 0⌝.
   Proof.
     destruct n.
     - iSplit; iIntros "H /="; auto.
@@ -29,6 +29,9 @@ Section own.
       rewrite /freeable_sz (proj2 (Qp_eq (mk_Qp _ _) 1)) //= Qcmult_inv_r //.
   Qed.
 
+  Lemma freeable_sz_full_S n l : freeable_sz (S n) (S n) l ⊣⊢ †{1}l…(S n).
+  Proof. rewrite freeable_sz_full. iSplit; auto. iIntros "[$|%]"; done. Qed.
+
   Lemma freeable_sz_split n sz1 sz2 l :
     freeable_sz n sz1 l ∗ freeable_sz n sz2 (shift_loc l sz1) ⊣⊢
                 freeable_sz n (sz1 + sz2) l.