diff --git a/theories/typing/examples/lazy_lft.v b/theories/typing/examples/lazy_lft.v
index 4d417260d5c054fd16620135916c3acec4372bb1..0ed4fd617819677fcd789f159dcd3c683f2ca72a 100644
--- a/theories/typing/examples/lazy_lft.v
+++ b/theories/typing/examples/lazy_lft.v
@@ -24,8 +24,8 @@ Section lazy_lft.
     iApply (type_newlft []). iIntros (α).
     iApply (type_new_subtype (Π[uninit 1;uninit 1])); [solve_typing..|].
       iIntros (t). simpl_subst.
-    iApply type_new; [solve_typing|]. iIntros (f). simpl_subst.
-    iApply type_new; [solve_typing|]. iIntros (g). simpl_subst.
+    iApply type_new; [solve_typing..|]. iIntros (f). simpl_subst.
+    iApply type_new; [solve_typing..|]. iIntros (g). simpl_subst.
     iApply type_int. iIntros (v42). simpl_subst.
     iApply type_assign; [solve_typing..|].
     iApply (type_assign _ (&shr{α}_)); [solve_typing..|].
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index 2220e79dd67e0a042e832fbfcb1996aaa264d4f4..d41c2925e967df26ff07bb67ae4a24a98e09eab3 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -287,6 +287,7 @@ Lemma elctx_sat_submseteq `{invG Σ, lftG Σ} E E' L :
   E' ⊆+ E → elctx_sat E L E'.
 Proof. iIntros (HE' ?) "_ !# H". by iApply big_sepL_submseteq. Qed.
 
+(* TODO: This is not really the right file for stuff like this. *)
 Hint Constructors Forall Forall2 elem_of_list : lrust_typing.
 Hint Resolve of_val_unlock : lrust_typing.
 Hint Resolve
@@ -299,6 +300,9 @@ Hint Resolve
 
 Hint Resolve elctx_sat_submseteq | 100 : lrust_typing.
 
+Hint Extern 1 (@eq nat _ (Z.to_nat _)) => (etrans; [symmetry; exact: Nat2Z.id | reflexivity]) : lrust_typing.
+Hint Extern 1 (@eq nat (Z.to_nat _) _) => (etrans; [exact: Nat2Z.id | reflexivity]) : lrust_typing.
+
 (* FIXME : I would prefer using a [Hint Resolve <-] for this, but
    unfortunately, this is not preserved across modules. See:
      https://coq.inria.fr/bugs/show_bug.cgi?id=5189
diff --git a/theories/typing/lib/cell.v b/theories/typing/lib/cell.v
index 9234d7f81d2f93538cf7d7da21b14bea1c1bb207..7b29d2216d6fce9156f02e2a83562f4539d83168 100644
--- a/theories/typing/lib/cell.v
+++ b/theories/typing/lib/cell.v
@@ -155,7 +155,7 @@ Section typing.
       iIntros (α ϝ ret arg). inv_vec arg=>c x. simpl_subst.
     iApply type_deref; [solve_typing..|].
     iIntros (c'); simpl_subst.
-    iApply type_new; [solve_typing..|]. iIntros (r); simpl_subst.
+    iApply type_new; [solve_typing..|]; iIntros (r); simpl_subst.
     (* Drop to Iris level. *)
     iIntros (tid) "#LFT #HE Htl HL HC".
     rewrite 3!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
@@ -170,11 +170,11 @@ Section typing.
     iDestruct (ty_size_eq with "Hrown") as ">Heq". iDestruct "Heq" as %Heq.
     (* FIXME: Changing the order of $Hr↦ $Hc'↦ breaks applying...?? *)
     wp_apply (wp_memcpy with "[$Hr↦ $Hc'↦]").
-    { by rewrite Heq Nat2Z.id. }
+    { by rewrite Heq. }
     { f_equal. done. }
     iIntros "[Hr↦ Hc'↦]". wp_seq.
     iDestruct "Hx" as "[Hx↦ Hx†]". iDestruct "Hx↦" as (vx) "[Hx↦ Hxown]".
-    rewrite Nat2Z.id. iDestruct (ty_size_eq with "Hxown") as "#%".
+    iDestruct (ty_size_eq with "Hxown") as "#%".
     wp_apply (wp_memcpy with "[$Hc'↦ $Hx↦]"); try by f_equal.
     iIntros "[Hc'↦ Hx↦]". wp_seq.
     iMod ("Hclose2" with "[Hc'↦ Hxown] Htl") as "[Htok Htl]"; first by auto with iFrame.
diff --git a/theories/typing/lib/mutex/mutex.v b/theories/typing/lib/mutex/mutex.v
index f064bed9b20cc5c440bcf4b2a8aa8c738f7cdf16..6f3c9bfab1ebedfb65e00daae87cc81de00432c9 100644
--- a/theories/typing/lib/mutex/mutex.v
+++ b/theories/typing/lib/mutex/mutex.v
@@ -104,8 +104,9 @@ Section code.
   Proof.
     intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (_ ϝ ret arg). inv_vec arg=>x. simpl_subst.
-    iApply type_new; [solve_typing..|]; iIntros (m); simpl_subst.
-    rewrite (Nat2Z.id (S ty.(ty_size))). (* FIXME: Having to do this after every type_new is rather annoying... *)
+    (* FIXME: It should be possible to infer the `S ty.(ty_size)` here.
+       This should be done in the @eq external hints added in lft_contexts.v. *)
+    iApply (type_new (S ty.(ty_size))); [solve_typing..|]; iIntros (m); simpl_subst.
     (* FIXME: The following should work.  We could then go into Iris later.
     iApply (type_memcpy ty); [solve_typing..|]. *)
     (* Switch to Iris. *)
@@ -145,8 +146,7 @@ Section code.
   Proof.
     intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (_ ϝ ret arg). inv_vec arg=>m. simpl_subst.
-    iApply type_new; [solve_typing..|]; iIntros (x); simpl_subst.
-    rewrite (Nat2Z.id ty.(ty_size)).
+    iApply (type_new ty.(ty_size)); [solve_typing..|]; iIntros (x); simpl_subst.
     (* Switch to Iris. *)
     iIntros (tid) "#LFT #HE Hna HL Hk [Hx [Hm _]]".
     rewrite !tctx_hasty_val /=.
diff --git a/theories/typing/lib/mutex/mutexguard.v b/theories/typing/lib/mutex/mutexguard.v
index 93c347f0efd38733ae923ece3a6c783413bc671b..ced23e5e477282cfc2ea80c24c4da9f7415a36fa 100644
--- a/theories/typing/lib/mutex/mutexguard.v
+++ b/theories/typing/lib/mutex/mutexguard.v
@@ -112,8 +112,7 @@ Section code.
     intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
     iApply type_deref; [solve_typing..|]; iIntros (m); simpl_subst.
-    iApply type_new; [solve_typing..|]; iIntros (g); simpl_subst.
-    rewrite (Nat2Z.id 1). (* Having to do this is rather annoying... *)
+    iApply (type_new 1); [solve_typing..|]; iIntros (g); simpl_subst.
     (* Switch to Iris. *)
     iIntros (tid) "#LFT #HE Hna HL Hk [Hg [Hx [Hm _]]]".
     rewrite !tctx_hasty_val [[x]]lock /=.
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index 3d9b2f04f5ca35ecc4a514ef19d9dc2e749f0e13..c16300cc3d8a0dc363e3a9e20a18710864b2d189 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -359,10 +359,10 @@ Section code.
   Proof.
     intros E L. 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.
+    iApply (type_new (2 + ty.(ty_size))); [solve_typing..|]; iIntros (rcbox); simpl_subst.
+    iApply (type_new 1); [solve_typing..|]; iIntros (rc); simpl_subst.
     iIntros (tid) "#LFT #HE Hna HL Hk [Hrc [Hrcbox [Hx _]]]".
-    rewrite (Nat2Z.id (2 + ty.(ty_size))) !tctx_hasty_val.
+    rewrite !tctx_hasty_val.
     iDestruct (ownptr_own with "Hx") as (lx vlx) "(% & Hx↦ & Hx & Hx†)". subst x.
     iDestruct (ownptr_uninit_own with "Hrcbox")
       as (lrcbox vlrcbox) "(% & Hrcbox↦ & Hrcbox†)". subst rcbox. inv_vec vlrcbox=>???.
@@ -402,8 +402,7 @@ Section code.
   Proof.
     intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
-    iApply type_new; [solve_typing..|]; iIntros (r); simpl_subst.
-    rewrite (Nat2Z.id 1). (* Having to do this is rather annoying... *)
+    iApply (type_new 1); [solve_typing..|]; iIntros (r); simpl_subst.
     iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
     iIntros (tid) "#LFT #HE Hna HL Hk [Hx [Hrc' [Hr _]]]".
     rewrite !tctx_hasty_val [[x]]lock.
@@ -466,7 +465,7 @@ Section code.
   Proof.
     intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ϝ ret arg). inv_vec arg=>rcx. simpl_subst.
-    iApply type_new; [solve_typing..|]; iIntros (x); simpl_subst. rewrite (Nat2Z.id 1).
+    iApply (type_new 1); [solve_typing..|]; iIntros (x); simpl_subst.
     iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
     iIntros (tid) "#LFT #HE Hna HL Hk [Hrcx [#Hrc' [Hx _]]]".
     rewrite !tctx_hasty_val [[rcx]]lock.
@@ -528,8 +527,7 @@ Section code.
     (* TODO: There is a *lot* of duplication between this proof and the one for drop. *)
     intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
     iIntros (_ ϝ ret arg). inv_vec arg=>rcx. simpl_subst.
-    iApply type_new; [solve_typing..|]; iIntros (r); simpl_subst.
-    rewrite (Nat2Z.id (Σ[ ty; rc ty ]).(ty_size)).
+    iApply (type_new (Σ[ ty; rc ty ]).(ty_size)); [solve_typing..|]; iIntros (r); simpl_subst.
     iApply (type_cont [] [ϝ ⊑ₗ []]
                       (λ _, [rcx ◁ box (uninit 1); r ◁ box (Σ[ ty; rc ty ])])) ;
       [solve_typing..| |]; last first.
@@ -623,8 +621,7 @@ Section code.
   Proof.
     intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
     iIntros (_ ϝ ret arg). inv_vec arg=>rcx. simpl_subst.
-    iApply type_new; [solve_typing..|]; iIntros (r); simpl_subst.
-    rewrite (Nat2Z.id (option ty).(ty_size)).
+    iApply (type_new (option ty).(ty_size)); [solve_typing..|]; iIntros (r); simpl_subst.
     iApply (type_cont [] [ϝ ⊑ₗ []]
                       (λ _, [rcx ◁ box (uninit 1); r ◁ box (option ty)]));
       [solve_typing..| |]; last first.
@@ -714,7 +711,7 @@ Section code.
   Proof.
     intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ϝ ret arg). inv_vec arg=>rcx. simpl_subst.
-    iApply type_new; [solve_typing..|]; iIntros (r); simpl_subst. rewrite (Nat2Z.id 2%nat).
+    iApply (type_new 2); [solve_typing..|]; iIntros (r); simpl_subst.
     iApply (type_cont [] [ϝ ⊑ₗ []]
                       (λ _, [rcx ◁ box (uninit 1); r ◁ box (option $ &uniq{α} ty)]));
       [solve_typing..| |]; last first.
@@ -835,7 +832,7 @@ Section code.
   Proof.
     intros Hclone E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ϝ ret arg). inv_vec arg=>rcx. simpl_subst.
-    iApply type_new; [solve_typing..|]; iIntros (r); simpl_subst. rewrite (Nat2Z.id 1%nat).
+    iApply (type_new 1); [solve_typing..|]; iIntros (r); simpl_subst.
     iApply (type_cont [] [ϝ ⊑ₗ []]
                       (λ _, [rcx ◁ box (uninit 1); r ◁ box (&uniq{α} ty)]));
       [solve_typing..| |]; last first.
diff --git a/theories/typing/lib/rc/weak.v b/theories/typing/lib/rc/weak.v
index 35e2364825e0cc09fd93bf29be9665ef279b3914..90b45aec53bb2b13d94d5efe1a0ef33a5f06ed56 100644
--- a/theories/typing/lib/rc/weak.v
+++ b/theories/typing/lib/rc/weak.v
@@ -129,8 +129,7 @@ Section code.
   Proof.
     intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ϝ ret arg). inv_vec arg=>w. simpl_subst.
-    iApply type_new; [solve_typing..|]; iIntros (r); simpl_subst.
-    rewrite (Nat2Z.id 2). (* Having to do this is rather annoying... *)
+    iApply (type_new 2); [solve_typing..|]; iIntros (r); simpl_subst.
     iApply (type_cont [] [ϝ ⊑ₗ []]
                       (λ _, [w ◁ box (&shr{α} weak ty); r ◁ box (option (rc ty))])) ;
       [solve_typing..| |]; last first.
@@ -241,8 +240,7 @@ Section code.
     (* TODO : this is almost identical to rc_clone *)
     intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
     iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
-    iApply type_new; [solve_typing..|]; iIntros (r); simpl_subst.
-    rewrite (Nat2Z.id 1). (* Having to do this is rather annoying... *)
+    iApply (type_new 1); [solve_typing..|]; iIntros (r); simpl_subst.
     iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
     iIntros (tid) "#LFT #HE Hna HL Hk [Hx [Hrc' [Hr _]]]".
     rewrite !tctx_hasty_val [[x]]lock.
@@ -304,8 +302,7 @@ Section code.
     (* TODO : this is almost identical to rc_clone *)
     intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
     iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
-    iApply type_new; [solve_typing..|]; iIntros (r); simpl_subst.
-    rewrite (Nat2Z.id 1). (* Having to do this is rather annoying... *)
+    iApply (type_new 1); [solve_typing..|]; iIntros (r); simpl_subst.
     iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
     iIntros (tid) "#LFT #HE Hna HL Hk [Hx [Hrc' [Hr _]]]".
     rewrite !tctx_hasty_val [[x]]lock.
@@ -456,10 +453,9 @@ Section code.
   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.
+    iApply (type_new (2 + ty.(ty_size))); [solve_typing..|]; iIntros (rcbox); simpl_subst.
+    iApply (type_new 1); [solve_typing..|]; iIntros (w); simpl_subst.
+    iIntros (tid) "#LFT #HE Hna HL Hk [Hw [Hrcbox _]]". rewrite !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]".
diff --git a/theories/typing/lib/refcell/refcell_code.v b/theories/typing/lib/refcell/refcell_code.v
index b68b7e895fb50288c8af0cc68e8d17c419125224..58e80365813c476c5d6e719d34785630c9951666 100644
--- a/theories/typing/lib/refcell/refcell_code.v
+++ b/theories/typing/lib/refcell/refcell_code.v
@@ -24,10 +24,9 @@ Section refcell_functions.
   Proof.
     intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (_ ϝ ret arg). inv_vec arg=>x. simpl_subst.
-    iApply type_new; [solve_typing..|].
+    iApply (type_new (S ty.(ty_size))); [solve_typing..|].
     iIntros (r tid) "#LFT #HE Hna HL Hk HT". simpl_subst.
-    rewrite (Nat2Z.id (S ty.(ty_size))) tctx_interp_cons
-            tctx_interp_singleton !tctx_hasty_val.
+    rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
     iDestruct "HT" as "[Hr Hx]".
     iDestruct (ownptr_own with "Hx") as (lx vlx) "(% & Hx↦ & Hx & Hx†)". subst x.
     iDestruct (ownptr_uninit_own with "Hr") as (lr vlr) "(% & Hr↦ & Hr†)". subst r.
@@ -59,10 +58,9 @@ Section refcell_functions.
   Proof.
     intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (_ ϝ ret arg). inv_vec arg=>x. simpl_subst.
-    iApply type_new; [solve_typing..|].
+    iApply (type_new ty.(ty_size)); [solve_typing..|].
     iIntros (r tid) "#LFT #HE Hna HL Hk HT". simpl_subst.
-    rewrite (Nat2Z.id (ty.(ty_size))) tctx_interp_cons
-            tctx_interp_singleton !tctx_hasty_val.
+    rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
     iDestruct "HT" as "[Hr Hx]".
     iDestruct (ownptr_own with "Hx") as (lx vlx) "(% & >Hx↦ & Hx & Hx†)". subst x.
     inv_vec vlx=>-[[|?|?]|????] vl; try iDestruct "Hx" as ">[]". simpl vec_to_list.
diff --git a/theories/typing/lib/rwlock/rwlock_code.v b/theories/typing/lib/rwlock/rwlock_code.v
index 1d81abac2c64e177ada4074cb4f961d67f4dc46f..7362d596d4a0eace986b261c4732a225ba5d4072 100644
--- a/theories/typing/lib/rwlock/rwlock_code.v
+++ b/theories/typing/lib/rwlock/rwlock_code.v
@@ -24,10 +24,9 @@ Section rwlock_functions.
   Proof.
     intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (_ ret ϝ arg). inv_vec arg=>x. simpl_subst.
-    iApply type_new; [solve_typing..|].
+    iApply (type_new (S ty.(ty_size))); [solve_typing..|].
     iIntros (r tid) "#LFT HE Hna HL Hk HT". simpl_subst.
-    rewrite (Nat2Z.id (S ty.(ty_size))) tctx_interp_cons
-            tctx_interp_singleton !tctx_hasty_val.
+    rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
     iDestruct "HT" as "[Hr Hx]". destruct x as [[|lx|]|]; try done.
     iDestruct "Hx" as "[Hx Hx†]". iDestruct "Hx" as (vl) "[Hx↦ Hx]".
     destruct r as [[|lr|]|]; try done. iDestruct "Hr" as "[Hr Hr†]".
@@ -60,10 +59,9 @@ Section rwlock_functions.
   Proof.
     intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (_ ret ϝ arg). inv_vec arg=>x. simpl_subst.
-    iApply type_new; [solve_typing..|].
+    iApply (type_new ty.(ty_size)); [solve_typing..|].
     iIntros (r tid) "#LFT HE Hna HL Hk HT". simpl_subst.
-    rewrite (Nat2Z.id (ty.(ty_size))) tctx_interp_cons
-            tctx_interp_singleton !tctx_hasty_val.
+    rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
     iDestruct "HT" as "[Hr Hx]". destruct x as [[|lx|]|]; try done.
     iDestruct "Hx" as "[Hx Hx†]".
     iDestruct "Hx" as ([|[[]|]vl]) "[Hx↦ Hx]"; try iDestruct "Hx" as ">[]".
diff --git a/theories/typing/own.v b/theories/typing/own.v
index f023f1e48d47f99bf631c8effb91e8bda70a7e51..db4fce97dd7153cefe4a871e96bb396e84e03376 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -257,13 +257,14 @@ Section typing.
     iExists vl. iFrame. by rewrite Nat2Z.id uninit_own.
   Qed.
 
-  Lemma type_new E L C T x (n : Z) e :
+  Lemma type_new {E L C T} (n' : nat) x (n : Z) e :
     Closed (x :b: []) e →
     0 ≤ n →
-    (∀ (v : val) (n' := Z.to_nat n),
+    n' = Z.to_nat n →
+    (∀ (v : val),
         typed_body E L C ((v ◁ own_ptr n' (uninit n')) :: T) (subst' x v e)) -∗
     typed_body E L C T (let: x := new [ #n ] in e).
-  Proof. iIntros. iApply type_let; [by apply type_new_instr|solve_typing..]. Qed.
+  Proof. iIntros. subst. iApply type_let; [by apply type_new_instr|solve_typing..]. Qed.
 
   Lemma type_new_subtype ty E L C T x (n : Z) e :
     Closed (x :b: []) e →
@@ -309,17 +310,18 @@ Section typing.
     (∀ (v : val), typed_body E L C ((v ◁ own_ptr 1 ty)::T') (subst x v e)) -∗
     typed_body E L C T (letalloc: x <- p in e).
   Proof.
-    iIntros. iApply type_new.
+    iIntros (??? Hsz) "**". iApply type_new.
     - rewrite /Closed /=. rewrite !andb_True.
       eauto 10 using is_closed_weaken with set_solver.
     - done.
-    - iIntros (xv) "/=".
+    - solve_typing.
+    - iIntros (xv) "/=". rewrite -Hsz.
       assert (subst x xv (x <- p ;; e)%E = (xv <- p ;; subst x xv e)%E) as ->.
       { (* TODO : simpl_subst should be able to do this. *)
         unfold subst=>/=. repeat f_equal.
         - by rewrite bool_decide_true.
         - eapply is_closed_subst. done. set_solver. }
-      iApply type_assign; [|solve_typing|by eapply write_own|done].
+      iApply type_assign; [|solve_typing|by eapply write_own|solve_typing].
       apply subst_is_closed; last done. apply is_closed_of_val.
   Qed.
 
@@ -335,6 +337,7 @@ Section typing.
     - rewrite /Closed /=. rewrite !andb_True.
       eauto 10 using is_closed_of_val, is_closed_weaken with set_solver.
     - lia.
+    - done.
     - iIntros (xv) "/=".
       assert (subst x xv (x <-{ty.(ty_size)} !p ;; e)%E =
               (xv <-{ty.(ty_size)} !p ;; subst x xv e)%E) as ->.