diff --git a/theories/typing/product_split.v b/theories/typing/product_split.v
index 154dca9f6e688d6fe2a454e22aea104ebfccb38f..dce282b4072ed5075cd5bac4c9e8f6b310d8c405 100644
--- a/theories/typing/product_split.v
+++ b/theories/typing/product_split.v
@@ -95,6 +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 "EQ" as %->. iSplitL "H↦1 H†1 H1".
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 89ffb4c61faeb4826c5af1cb7ec3fe6b839cd05b..31c53a2ba69ac68706f8e9afea4cd88d16030cca 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -50,6 +50,11 @@ 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
     | 0%nat => ∅
@@ -99,7 +104,6 @@ Section type.
     rewrite shr_locsE_shift na_own_union //. apply shr_locsE_disj.
   Qed.
 
-  (** Copy types *)
   Class Copy (t : type) := {
     copy_persistent tid vl : PersistentP (t.(ty_own) tid vl);
     copy_shr_acc κ tid E F l q :
diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v
index e20a4f686fd994568680be66400a4c179b702df4..cf019f8a611c72cb66f37cac94f3d4d09733d44a 100644
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
@@ -7,7 +7,6 @@ Set Default Proof Using "Type".
 
 Section uniq_bor.
   Context `{typeG Σ}.
-
   Local Hint Extern 1000 (_ ⊆ _) => set_solver : ndisj.
 
   Program Definition uniq_bor (κ:lft) (ty:type) :=