try and fail to make using ty_size_eq on \later own more convenient

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".

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 :

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) :=