diff --git a/theories/typing/own.v b/theories/typing/own.v
index b1854cdcf6fc697fd1e3bda688ab2e5182c2296c..8f64431d7bf85df7b05fb90c931807ed27630a42 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -162,12 +162,9 @@ Section typing.
   Proof.
     iIntros (Hsz) "!#". iIntros (p tid F qE qL ?) "_ $ $ Hown". iDestruct "Hown" as (l) "(Heq & H↦ & H†)".
     iDestruct "Heq" as %[= ->]. iDestruct "H↦" as (vl) "[>H↦ Hown]".
-    (* This turns out to be the fastest way to apply a lemma below â–· -- at
-    least if we're fine throwing away the premise even though the result
-    is persistent, which in this case, we are. *)
-    rewrite ty'.(ty_size_eq). iDestruct "Hown" as ">%". iModIntro.
+    iDestruct (ty_size_eq with "Hown") as "#>%".  iModIntro.
     iExists _, _. iFrame "H↦".
-    iSplit; first by rewrite Hsz. iIntros "Hown !>".
+    iSplit; first by rewrite Hsz. iIntros "Hown' !>".
     iExists _. iSplit; first done. rewrite Hsz. iFrame.
   Qed.
 
@@ -185,8 +182,7 @@ Section typing.
   Proof.
     iAlways. iIntros (p tid F qE qL ?) "_ $ $ $ Hown". iDestruct "Hown" as (l) "(Heq & H↦ & H†)".
     iDestruct "Heq" as %[= ->]. iDestruct "H↦" as (vl) "[>H↦ Hown]".
-    iAssert (▷ ⌜length vl = ty_size ty⌝)%I with "[#]" as ">%".
-    { by iApply ty_size_eq. }
+    iDestruct (ty_size_eq with "Hown") as "#>%".
     iModIntro. iExists l, vl, _. iSplit; first done. iFrame "∗#". iIntros "Hl !>".
     iExists _. iSplit; first done. iFrame "H†". iExists _. iFrame.
     iApply uninit_own. auto.
@@ -235,7 +231,7 @@ Section typing.
     wp_bind p. iApply (wp_hasty with "Hp"). iIntros (v) "_ Hown".
     iDestruct "Hown" as (l) "(Hv & H↦∗: & >H†)". iDestruct "Hv" as %[=->].
     iDestruct "H↦∗:" as (vl) "[>H↦ Hown]". rewrite tctx_interp_nil.
-    rewrite ty_size_eq. iDestruct "Hown" as ">Hown". iDestruct "Hown" as %<-.
+    iDestruct (ty_size_eq with "Hown") as "#>EQ". iDestruct "EQ" as %<-.
     iApply (wp_delete with "[-]"); try (by auto); [].
     rewrite freeable_sz_full. by iFrame.
   Qed.
diff --git a/theories/typing/product.v b/theories/typing/product.v
index f91ba5cd359b372c0c74296b445ffed2e38ac75e..9cfb6a6586502d9bfca2d05a2f1b635bb9dbad02 100644
--- a/theories/typing/product.v
+++ b/theories/typing/product.v
@@ -120,10 +120,8 @@ Section product.
     destruct (Qp_lower_bound q1 q2) as (qq & q'1 & q'2 & -> & ->). iExists qq.
     iDestruct "H1" as (vl1) "[H↦1 H1]". iDestruct "H2" as (vl2) "[H↦2 H2]".
     rewrite !split_prod_mt.
-    iAssert (▷ ⌜length vl1 = ty1.(ty_size)⌝)%I with "[#]" as ">%".
-    { iNext. by iApply ty_size_eq. }
-    iAssert (▷ ⌜length vl2 = ty2.(ty_size)⌝)%I with "[#]" as ">%".
-    { iNext. by iApply ty_size_eq. }
+    iDestruct (ty_size_eq with "H1") as "#>%".
+    iDestruct (ty_size_eq with "H2") as "#>%".
     iDestruct "H↦1" as "[H↦1 H↦1f]". iDestruct "H↦2" as "[H↦2 H↦2f]".
     iIntros "!>". iSplitL "H↦1 H1 H↦2 H2".
     - iNext. iSplitL "H↦1 H1". iExists vl1. by iFrame. iExists vl2. by iFrame.
diff --git a/theories/typing/product_split.v b/theories/typing/product_split.v
index dce282b4072ed5075cd5bac4c9e8f6b310d8c405..9687d8cdbf2f3f436595574c16bb6426008da43b 100644
--- a/theories/typing/product_split.v
+++ b/theories/typing/product_split.v
@@ -95,9 +95,7 @@ Section product_split.
     iDestruct "H" as (vl1 vl2) "(>% & H1 & H2)". subst.
     rewrite heap_mapsto_vec_app -freeable_sz_split.
     iDestruct "H†" as "[H†1 H†2]". iDestruct "H↦" as "[H↦1 H↦2]".
-    (* FIXME: I found no way to use ty_size_eq_later here to avoid the assert. *)
-    iAssert (▷ ⌜length vl1 = ty_size ty1⌝)%I with "[#]" as ">EQ".
-    { iNext. by iApply ty_size_eq. }
+    iDestruct (ty_size_eq with "H1") as "#>EQ".
     iDestruct "EQ" as %->. iSplitL "H↦1 H†1 H1".
     + iExists _. iSplitR. done. iExists _. iFrame. iSplitL ""; first done.
       iExists _. iFrame. done.
@@ -119,8 +117,7 @@ Section product_split.
     iSplitR; first done. rewrite -freeable_sz_split. iFrame.
     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.
-    iAssert (▷ ⌜length vl1 = ty_size ty1⌝)%I with "[#]" as ">EQ".
-    { iNext. by iApply ty_size_eq. }
+    iDestruct (ty_size_eq with "H1") as "#>EQ".
     iDestruct "EQ" as %->. iFrame. iExists vl1, vl2. iFrame. auto.
   Qed.
 
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index 8a24832e2b79e771d309b942c7ad747b09d6e3bf..8b0844c9ddda6298bff8d72cc751d763f7e701a0 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -249,8 +249,7 @@ Section typing_rules.
       as (l1 vl1) "([% %] & Hl1 & Hcl1)"; first done.
     iMod ("Hread" with "* [] LFT Htl HE2 HL2 Hown2")
       as (l2 vl2 q2) "(% & Hl2 & Hown2 & Hcl2)"; first done.
-    iAssert (▷⌜length vl2 = ty.(ty_size)⌝)%I with "[#]" as ">%".
-    { by iApply ty_size_eq. } subst v1 v2. iApply wp_fupd.
+    iDestruct (ty_size_eq with "Hown2") as "#>%". subst v1 v2. iApply wp_fupd.
     iApply (wp_memcpy with "[$HEAP $Hl1 $Hl2]"); first done; try congruence; [].
     iNext. iIntros "[Hl1 Hl2]". iApply ("HΦ" with ">"). rewrite !tctx_hasty_val' //.
     iMod ("Hcl1" with "[Hl1 Hown2]") as "($ & $ & $)".
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index d2da2e67386b708d646f2690de53265197c29db7..af2abac39861bb1d5600fb161ef75dbb1b65eca8 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -54,16 +54,15 @@ Section sum.
     iSplit; iIntros "H".
     - iDestruct "H" as (vl) "[Hmt Hown]". iDestruct "Hown" as (i vl' vl'') "(% & % & Hown)".
       subst. iExists i. iDestruct (heap_mapsto_vec_cons with "Hmt") as "[$ Hmt]".
-      iAssert (⌜length vl' = (nth i tyl ∅).(ty_size)⌝%I) as %Hvl'.
-      { iApply ty_size_eq. done. }
+      iDestruct (ty_size_eq with "Hown") as "#EQ". iDestruct "EQ" as %Hvl'.
       iDestruct (heap_mapsto_vec_app with "Hmt") as "[Hmt Htail]". iSplitL "Htail".
       + iExists vl''. rewrite (shift_loc_assoc_nat _ 1) Hvl'. iFrame. iPureIntro.
         rewrite -Hvl'. simpl in *. rewrite -app_length. congruence.
       + iExists vl'. by iFrame.
     - iDestruct "H" as (i) "[[Hmt1 Htail] Hown]".
       iDestruct "Hown" as (vl') "[Hmt2 Hown]". iDestruct "Htail" as (vl'') "[Hmt3 %]".
-      iAssert (⌜length vl' = (nth i tyl ∅).(ty_size)⌝%I) as %Hvl'.
-      { iApply ty_size_eq. done. } iExists (#i::vl'++vl'').
+      iDestruct (ty_size_eq with "Hown") as "#EQ". iDestruct "EQ" as %Hvl'.
+      iExists (#i::vl'++vl'').
       rewrite heap_mapsto_vec_cons heap_mapsto_vec_app (shift_loc_assoc_nat _ 1) Hvl'.
       iFrame. iExists i, vl', vl''. iSplit; first done. iFrame. iPureIntro.
       simpl. f_equal. by rewrite app_length Hvl'.
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 31c53a2ba69ac68706f8e9afea4cd88d16030cca..eb076a1b547a0b9cf8112c9942ec970ca6493d9d 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -50,10 +50,6 @@ Section type.
     }.
   Global Existing Instances ty_shr_persistent.
 
-  Lemma ty_size_eq_later (ty : type) tid vl :
-    ▷ ty.(ty_own) tid vl -∗ ▷ ⌜length vl = ty.(ty_size)⌝.
-  Proof. iIntros "Hown". iApply ty_size_eq. done. Qed.
-
   (** Copy types *)
   Fixpoint shr_locsE (l : loc) (n : nat) : coPset :=
     match n with
diff --git a/theories/typing/type_sum.v b/theories/typing/type_sum.v
index 93f37f87d7066e8b35da37ca99649996b068c6f0..176924bfbaca817375e335f9fc6e5deaaa2b15b8 100644
--- a/theories/typing/type_sum.v
+++ b/theories/typing/type_sum.v
@@ -244,7 +244,7 @@ Section case.
       - specialize (IHtyl i). intuition lia. }
     rewrite -(take_drop (ty.(ty_size)) vl1) heap_mapsto_vec_app.
     iDestruct "H↦vl1" as "[H↦vl1 H↦pad]".
-    iAssert (▷ ⌜length vl2 = ty.(ty_size)⌝)%I with "[#]" as ">%". by rewrite -ty_size_eq.
+    iDestruct (ty_size_eq with "Hty") as "#>%".
     iApply wp_fupd. iApply (wp_memcpy with "[$HEAP $H↦vl1 $H↦2]"); try done.
     { rewrite take_length. lia. }
     iNext; iIntros "[H↦vl1 H↦2]".
diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v
index 0a515948822093e23ac5a0ff9ff2f423b7de23c2..f172818914a99c61871a8f9183edd56f8be7f87b 100644
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
@@ -229,9 +229,8 @@ Section typing.
     iMod (bor_iff with "LFT [] H↦") as "H↦". set_solver. by eauto.
     iMod (bor_acc with "LFT H↦ Hκ") as "[H↦ Hclose']"; first set_solver.
     iDestruct "H↦" as (vl) "[>H↦ #Hown]".
-    iAssert (▷ ⌜length vl = ty_size ty⌝)%I with "[#]" as ">%".
-     { by iApply ty.(ty_size_eq). }
-    iIntros "!>". iExists _, _, _. iSplit; first done. iFrame "∗#". iIntros "H↦".
+    iDestruct (ty_size_eq with "Hown") as "#>%". iIntros "!>".
+    iExists _, _, _. iSplit; first done. iFrame "∗#". iIntros "H↦".
     iMod ("Hclose'" with "[H↦]") as "[H↦ Htok]". by iExists _; iFrame.
     iMod ("Hclose" with "Htok") as "($ & $ & $)".
     iExists _, _. erewrite <-uPred.iff_refl. auto.
diff --git a/theories/typing/unsafe/cell.v b/theories/typing/unsafe/cell.v
index 92fcd931f6c9efd49d1d9e0e032c64211acfd540..3dcc6ffe86c5794c1678e268cf74b9165b02d1b4 100644
--- a/theories/typing/unsafe/cell.v
+++ b/theories/typing/unsafe/cell.v
@@ -107,10 +107,8 @@ Section typing.
       iDestruct "Hown" as (vl') "[>H↦' Hown']".
       iMod (na_bor_acc with "LFT Hshr HE Htl") as "(Hown & Htl & Hclose)"; [solve_ndisj..|].
       iDestruct "Hown" as (vl) "[>H↦ Hown]".
-      iAssert (▷ ⌜length vl = ty_size ty⌝)%I with "[#]" as ">%".
-      { iNext. by iApply ty_size_eq. }
-      iAssert (▷ ⌜length vl' = ty_size ty⌝)%I with "[#]" as ">%".
-      { iNext. by iApply ty_size_eq. }
+      iDestruct (ty_size_eq with "Hown") as "#>%".
+      iDestruct (ty_size_eq with "Hown'") as "#>%".
       iApply wp_fupd. iApply (wp_memcpy with "[$HEAP $H↦ $H↦']"); [done..|].
       iNext. iIntros "[H↦ H↦']". rewrite {1}/elctx_interp big_opL_singleton /=.
       iMod ("Hclose" with "[H↦ Hown'] Htl") as "[$ $]".
@@ -128,5 +126,5 @@ Section typing.
     eapply (type_jump [_]); solve_typing.
   Qed.
 
-  (* TODO: potentially more operations? *)
+  (* TODO: get_mut *)
 End typing.