diff --git a/theories/typing/function.v b/theories/typing/function.v
index 0b40d59f63bda4b24e1dcf0a93a0f6ba54f41046..66423631d4e5a97fddcdc0607c1bb2e84740e461 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -232,8 +232,6 @@ Section typing.
     rewrite /typed_body. iNext. iIntros "*". iApply "Hf".
   Qed.
 
-  From iris.proofmode Require Import environments. (* FIXME: remove. *)
-
   (* In principle, proving this hard-coded to an empty L would be sufficient --
      but then we would have to require elctx_sat as an Iris assumption. *)
   Lemma type_call_iris' E L (κs : list lft) {A} x qκs qL tid
@@ -276,8 +274,7 @@ Section typing.
       { iApply (bor_fracture with "LFT"); first done. by rewrite Qp_mult_1_r. }
       iApply ("Hf" with "LFT [] Htl [Htk] [Hk HκsI HL]").
       + iApply "HE'". iIntros "{$# Hf Hinh HE' LFT HE %}".
-        iInduction κs as [|κ κs] "IH" forall "Hκs"=> //=.
-        iSplitL.
+        iInduction κs as [|κ κs] "IH" forall "Hκs"=> //=. iSplitL.
         { iApply lft_incl_trans; first done. iApply lft_intersect_incl_l. }
         iApply "IH". iAlways. iApply lft_incl_trans; first done. iApply lft_intersect_incl_r.
       + iSplitL; last done. iExists ϝ. iSplit; first by rewrite /= left_id.
diff --git a/theories/typing/lib/arc.v b/theories/typing/lib/arc.v
index f1cb0b133e1e08f9f4b5bc611933f7cdc5aa759e..8722a3fd1cdf11a7aa4af280af5ef134a08ca4d9 100644
--- a/theories/typing/lib/arc.v
+++ b/theories/typing/lib/arc.v
@@ -751,7 +751,7 @@ Section arc.
     iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
     iApply (type_sum_unit (option ty)); [solve_typing..|].
     iIntros (tid) "#LFT #HE Hna HL Hk [Hr [Hrcx [Hrc' _]]]".
-    rewrite !tctx_hasty_val [[rcx]]lock [[r]]lock. destruct rc' as [[|rc'|]|]=>//=.
+    rewrite !tctx_hasty_val. destruct rc' as [[|rc'|]|]=>//=.
     iAssert (shared_arc_own rc' ty tid)%I with "[>Hrc']" as "Hrc'".
     { iDestruct "Hrc'" as "[?|$]"; last done. iApply arc_own_share; solve_ndisj. }
     iDestruct "Hrc'" as (γ ν q) "(#Hpersist & Htok & Hν)".
@@ -759,7 +759,9 @@ Section arc.
       [by iDestruct "Hpersist" as "[$?]"|done|].
     iNext. iIntros (b) "Hdrop". wp_bind (if: _ then _ else _)%E.
     iApply (wp_wand _ _ (λ _, ty_own (box (option ty)) tid [r])%I with "[Hdrop Hr]").
-    { unlock. destruct b; wp_if=>//. destruct r as [[]|]=>//=.
+    { destruct b; wp_if=>//. destruct r as [[]|]; try done.
+      (* FIXME: 'simpl' reveals a match here.  Didn't we forbid that for ty_own? *)
+      rewrite {3}[option]lock. simpl. rewrite -{2 3}lock. (* FIXME: Tried using contextual pattern, did not work. *)
       iDestruct "Hr" as "[Hr ?]". iDestruct "Hr" as ([|d vl]) "[H↦ Hown]";
         first by iDestruct "Hown" as (???) "[>% ?]".
       rewrite heap_mapsto_vec_cons. iDestruct "H↦" as "[H↦0 H↦1]".
@@ -772,8 +774,8 @@ Section arc.
       iDestruct "Hlen" as %[= ?]. iApply (wp_memcpy with "[$H↦1 $H↦]"); [congruence..|].
       iNext. iIntros "[? Hrc']". wp_seq. iMod ("Hdrop" with "[Hrc' H†]") as "Htok".
       { unfold P2. auto with iFrame. }
-      wp_apply (drop_weak_spec with "[//] Htok"). iIntros ([]); last first.
-      { iIntros "_". wp_if. iFrame. iExists (_::_). rewrite heap_mapsto_vec_cons.
+      wp_apply (drop_weak_spec with "[//] Htok"). unlock. iIntros ([]); last first.
+      { iIntros "_". wp_if. unlock. iFrame. iExists (_::_). rewrite heap_mapsto_vec_cons.
         iFrame. iExists 1%nat, _, []. rewrite /= right_id_L Max.max_0_r.
         auto 10 with iFrame. }
       iIntros "([H† H1] & H2 & H3)". iDestruct "H1" as (vl') "[H1 Heq]".
@@ -820,7 +822,7 @@ Section arc.
       rewrite !heap_mapsto_vec_cons shift_loc_assoc. iFrame. auto. }
     iIntros (?) "_". wp_seq.
     (* Finish up the proof. *)
-    iApply (type_type _ _ _ [ rcx ◁ box (uninit 1); r ◁ box unit ]
+    iApply (type_type _ _ _ [ rcx ◁ box (uninit 1); r ◁ box (uninit 0) ]
             with "[] LFT HE Hna HL Hk [-]"); last first.
     { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val. unlock. iFrame.
       by rewrite tctx_hasty_val. }
@@ -862,7 +864,7 @@ Section arc.
     iIntros ([]) "H"; wp_if.
     - iDestruct "H" as "[Hν Hend]". rewrite -(lock [r]). destruct r as [[|r|]|]=>//=.
       iDestruct "Hr" as "[Hr >Hfree]". iDestruct "Hr" as (vl0) "[>Hr Hown]".
-      rewrite uninit_own. iDestruct "Hown" as ">Hlen".
+      iDestruct "Hown" as ">Hlen".
       destruct vl0 as [|? vl0]=>//; iDestruct "Hlen" as %[=Hlen0].
       rewrite heap_mapsto_vec_cons. iDestruct "Hr" as "[Hr0 Hr1]".
       iDestruct "Hpersist" as "(Ha & _ & H†)". wp_bind (_ <- _)%E.
@@ -1143,4 +1145,4 @@ Section arc.
       iApply type_delete; [solve_typing..|].
       iApply type_jump; solve_typing.
   Qed.
-End arc.
\ No newline at end of file
+End arc.
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index bf871939879c4c5a349a5f05394f6c78f315f369..5594c87835522b1579d71df5d1b04bceedbf4a52 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -712,13 +712,13 @@ Section code.
         { unlock. rewrite 3!tctx_interp_cons tctx_interp_singleton. iFrame "Hr Hrc".
           rewrite 1!tctx_hasty_val tctx_hasty_val' //. iFrame "Hrcx".
           rewrite shift_loc_0 /=. iFrame. iExists [_; _].
-          rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton uninit_own.
+          rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
           auto with iFrame. }
         iApply (type_delete (Π[uninit 2;uninit ty.(ty_size)])); [solve_typing..|].
         iApply type_jump; solve_typing.
       + rewrite (tctx_hasty_val' _ (#rc' +â‚— #2)); last done.
         iDestruct "Hrc" as "[Hrc H†2]". wp_op=>[?|_]. lia. wp_if. wp_op. wp_op. wp_write.
-        setoid_rewrite uninit_own. iMod ("Hproto" with "[H†1 H†2] H↦weak Hrc") as "Hna".
+        iMod ("Hproto" with "[H†1 H†2] H↦weak Hrc") as "Hna".
         { rewrite -freeable_sz_full_S -(freeable_sz_split _ 2 ty.(ty_size)). iFrame. }
         iApply (type_type _ _ _
              [ r ◁ own_ptr (ty_size Σ[ ty; rc ty ]) (Σ[ ty; rc ty]);
@@ -807,13 +807,13 @@ Section code.
         { unlock. rewrite 3!tctx_interp_cons tctx_interp_singleton. iFrame "Hr Hrc".
           rewrite 1!tctx_hasty_val tctx_hasty_val' //. iFrame "Hrcx".
           rewrite shift_loc_0 /=. iFrame. iExists [_; _].
-          rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton uninit_own.
+          rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
           auto with iFrame. }
         iApply (type_delete (Π[uninit 2;uninit ty.(ty_size)])); [solve_typing..|].
         iApply type_jump; solve_typing.
       + rewrite (tctx_hasty_val' _ (#rc' +â‚— #2)); last done.
         iDestruct "Hrc" as "[Hrc H†2]". wp_op=>[?|_]. lia. wp_if. wp_op. wp_op. wp_write.
-        setoid_rewrite uninit_own. iMod ("Hproto" with "[H†1 H†2] H↦weak Hrc") as "Hna".
+        iMod ("Hproto" with "[H†1 H†2] H↦weak Hrc") as "Hna".
         { rewrite -freeable_sz_full_S -(freeable_sz_split _ 2 ty.(ty_size)). iFrame. }
         iApply (type_type _ _ _
              [ r ◁ own_ptr (ty_size (option ty)) (option ty); rcx ◁ box (uninit 1) ]
diff --git a/theories/typing/lib/rc/weak.v b/theories/typing/lib/rc/weak.v
index 456d4a80cafc08efd632f5527d20fcdcfdb0e114..34417e1cd5f7f8cbd6535e4551c91ee1de538f2a 100644
--- a/theories/typing/lib/rc/weak.v
+++ b/theories/typing/lib/rc/weak.v
@@ -185,7 +185,7 @@ Section code.
           with "[] LFT HE Hna HL Hk [-]"); last first.
       { rewrite 2!tctx_interp_cons tctx_interp_singleton tctx_hasty_val !tctx_hasty_val' //.
         unlock. iFrame "Hr† Hw". iSplitL "Hr1 Hr2".
-        - setoid_rewrite uninit_own. iExists [_;_].
+        - iExists [_;_].
           rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton. auto with iFrame.
         - iRight. auto with iFrame. }
       iApply (type_sum_assign (option (rc ty))); [solve_typing..|].
@@ -202,7 +202,7 @@ Section code.
       iApply (type_type _ _ _ [ w ◁ box (&shr{α} weak ty); #lr ◁ box (uninit 2) ]
           with "[] LFT HE Hna HL Hk [-]"); last first.
       { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
-        unlock. iFrame. setoid_rewrite uninit_own. iExists [_;_].
+        unlock. iFrame. iExists [_;_].
         rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton. auto with iFrame. }
       iApply (type_sum_unit (option (rc ty))); [solve_typing..|].
       iApply type_jump; solve_typing.
@@ -218,7 +218,7 @@ Section code.
       iApply (type_type _ _ _ [ w ◁ box (&shr{α} weak ty); #lr ◁ box (uninit 2) ]
           with "[] LFT HE Hna HL Hk [-]"); last first.
       { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
-        unlock. iFrame. setoid_rewrite uninit_own. iExists [_;_].
+        unlock. iFrame. iExists [_;_].
         rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton. auto with iFrame. }
       iApply (type_sum_unit (option (rc ty))); [solve_typing..|].
       iApply type_jump; solve_typing.
@@ -427,9 +427,9 @@ Section code.
       { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
         unlock. iFrame. iDestruct "H" as (?) "(? & H↦ & ?)". iDestruct "H↦" as (?) "[? %]".
         rewrite /= freeable_sz_full_S. iFrame. iExists (_::_::_).
-        rewrite 2!heap_mapsto_vec_cons shift_loc_assoc uninit_own. iFrame.
-        iIntros "!>!%". simpl. congruence. }
-      iApply type_delete; [solve_typing..|].
+        rewrite 2!heap_mapsto_vec_cons shift_loc_assoc. iFrame.
+        iIntros "!> !%". simpl. congruence. }
+      iApply type_delete; [try solve_typing..|].
       iApply type_jump; solve_typing.
     - wp_read. wp_let. wp_op=>[|_]; first lia. wp_if. wp_op. wp_op. wp_write.
       iMod ("Hclose" with "Hlw") as "Hna".
diff --git a/theories/typing/own.v b/theories/typing/own.v
index db4fce97dd7153cefe4a871e96bb396e84e03376..47db32f457251651d7f7e3e2d0e19aea48648ebd 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -209,7 +209,7 @@ Section util.
     - iIntros "H". iDestruct "H" as (vl) "(% & Hl & _ & $)". subst v.
       iExists vl. iSplit; done.
     - iIntros "H". iDestruct "H" as (vl) "(% & Hl & $)". subst v.
-      iExists vl. rewrite uninit_own vec_to_list_length.
+      iExists vl. rewrite /= vec_to_list_length.
       eauto with iFrame.
   Qed.
 End util.
@@ -242,7 +242,7 @@ Section typing.
     iDestruct "Hown" as "[H↦ H†]". iDestruct "H↦" as (vl) "[>H↦ Hown]".
     iDestruct (ty_size_eq with "Hown") as "#>%".
     iExists l, vl, _. iFrame "∗#". iSplitR; first done. iIntros "!> Hl !> !>".
-    iExists _. iFrame. by iApply uninit_own.
+    iExists _. iFrame. done.
   Qed.
 
   Lemma type_new_instr {E L} (n : Z) :
@@ -254,7 +254,7 @@ Section typing.
     iApply wp_new; first done. iModIntro.
     iIntros (l vl) "(% & H† & Hlft)". subst. rewrite tctx_interp_singleton tctx_hasty_val.
     iNext. rewrite freeable_sz_full Z2Nat.id //. iFrame.
-    iExists vl. iFrame. by rewrite Nat2Z.id uninit_own.
+    iExists vl. iFrame. by rewrite Nat2Z.id.
   Qed.
 
   Lemma type_new {E L C T} (n' : nat) x (n : Z) e :
diff --git a/theories/typing/product.v b/theories/typing/product.v
index b93c3bd23651d86422eff70c0ef0eb71f570a8e3..84d714a8360e915bea8c5492f4ad32c22c290826 100644
--- a/theories/typing/product.v
+++ b/theories/typing/product.v
@@ -6,6 +6,9 @@ Set Default Proof Using "Type".
 Section product.
   Context `{typeG Σ}.
 
+  (* "Pre"-unit.  We later define the full unit as the empty product.  That's
+     convertible, but products are opaque in some hint DBs, so this does make a
+     difference. *)
   Program Definition unit0 : type :=
     {| ty_size := 0; ty_own tid vl := ⌜vl = []⌝%I; ty_shr κ tid l := True%I |}.
   Next Obligation. iIntros (tid vl) "%". by subst. Qed.
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index 1b88e917e6034800cef5044398a47b9d11aebca1..c2da2ff952eab94d4b891a4ff9553f02cf07e05d 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -127,7 +127,7 @@ Section sum.
     { clear EQmax. induction EQ as [|???? EQ _ IH]=>-[|i] //=. }
     constructor; simpl.
     - by rewrite EQmax.
-    - intros tid vl. rewrite /ty_own /= EQmax.
+    - intros tid vl. rewrite EQmax.
       solve_proper_core ltac:(fun _ => exact:EQnth || f_equiv).
     - intros κ tid l. unfold is_pad. rewrite EQmax.
       solve_proper_core ltac:(fun _ => exact:EQnth || (eapply ty_size_ne; try reflexivity) || f_equiv).
diff --git a/theories/typing/type.v b/theories/typing/type.v
index aa4fc4149d7af8e3fd8c586eb6721f54ce66d689..7adb46bcc1a35be23e443e5ad2d6a600222a0500 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -51,7 +51,7 @@ Instance: Params (@ty_size) 2.
 Instance: Params (@ty_own) 2.
 Instance: Params (@ty_shr) 2.
 
-Arguments ty_own {_ _} _ _ !_ / : simpl nomatch.
+Arguments ty_own {_ _} !_ _ _ / : simpl nomatch.
 
 Class TyWf `{typeG Σ} (ty : type) := { ty_lfts : list lft; ty_wf_E : elctx }.
 Arguments ty_lfts {_ _} _ {_}.
@@ -370,7 +370,7 @@ Section type_contractive.
   Proof.
     intros ???. constructor.
     - done.
-    - intros. destruct n; first done; simpl. f_equiv. f_equiv. done.
+    - intros. destruct n; first done; simpl. f_equiv. done.
     - intros. solve_contractive.
   Qed.
 End type_contractive.
diff --git a/theories/typing/type_sum.v b/theories/typing/type_sum.v
index dfa4a4385c64a0525797b506339fa9f0ec443cc1..5740b779256ab42623f7bd6d29ed0119339422b5 100644
--- a/theories/typing/type_sum.v
+++ b/theories/typing/type_sum.v
@@ -35,13 +35,13 @@ Section case.
     - rewrite /own_ptr /=. iDestruct (ty.(ty_size_eq) with "Hown") as %<-.
       iSplitL "H↦i Hfi"; last iSplitR "H↦vl'' Hfvl''".
       + rewrite shift_loc_0. iFrame. iExists [ #i]. rewrite heap_mapsto_vec_singleton.
-        iFrame. iExists [_], []. auto.
+        iFrame. auto.
       + eauto with iFrame.
       + rewrite -EQlen app_length minus_plus -(shift_loc_assoc_nat _ 1).
-        iFrame. iExists _. iFrame. rewrite uninit_own. auto.
+        iFrame. iExists _. iFrame. auto.
     - rewrite /= -EQlen app_length -(Nat.add_1_l (_+_)) -!freeable_sz_split. iFrame.
       iExists (#i :: vl' ++ vl''). iNext. rewrite heap_mapsto_vec_cons heap_mapsto_vec_app.
-      iFrame. iExists i, vl', vl''. rewrite /= -EQlen app_length nth_lookup EQty /=. auto.
+      iFrame. iExists i, vl', vl''. rewrite /= app_length nth_lookup EQty /=. auto.
   Qed.
 
   Lemma type_case_own E L C T T' p n tyl el :
diff --git a/theories/typing/uninit.v b/theories/typing/uninit.v
index b8852230083a62bfcaeac3e7c47d88c62ecadd6f..28875d508995b63e6d3007e02a4a93a2b9c9e463 100644
--- a/theories/typing/uninit.v
+++ b/theories/typing/uninit.v
@@ -19,13 +19,32 @@ Section uninit.
   Lemma uninit0_sz n : ty_size (uninit0 n) = n.
   Proof. induction n=>//=. by f_equal. Qed.
 
-  (* We redefine uninit as an alias of uninit0, so that the size
-     computes directly to [n] *)
+  Lemma uninit0_own n tid vl :
+    ty_own (uninit0 n) tid vl ⊣⊢ ⌜length vl = n⌝.
+  Proof.
+    iSplit.
+    - iIntros "Hvl".
+      iInduction n as [|n] "IH" forall (vl); simpl.
+      + iDestruct "Hvl" as "%". subst vl. done.
+      + iDestruct "Hvl" as (vl1 vl2) "(% & % & Hprod)".
+        destruct vl1 as [|v [|]]; try done. subst vl. simpl.
+        iDestruct ("IH" with "Hprod") as "%". iPureIntro. by f_equal.
+    - iIntros "%". subst n. iInduction vl as [|v vl] "IH"; first done.
+      simpl. iExists [v], vl. auto.
+  Qed.
+
+  (* We redefine uninit as an alias of uninit0, so that ty_size and ty_own
+     compute directly.  We re-use the sharing from the product as that saves a whole
+     lot of work. *)
   Program Definition uninit (n : nat) : type :=
-    {| ty_size := n; ty_own := (uninit0 n).(ty_own);
+    {| ty_size := n; ty_own tid vl := ⌜length vl = n⌝%I;
        ty_shr := (uninit0 n).(ty_shr) |}.
-  Next Obligation. intros. by rewrite ty_size_eq uninit0_sz. Qed.
-  Next Obligation. intros. by apply ty_share. Qed.
+  Next Obligation. iIntros (???) "%". done. Qed.
+  Next Obligation.
+    iIntros (???????) "LFT Hvl". iApply (ty_share (uninit0 n) with "LFT"); first done.
+    iApply (bor_iff with "[] Hvl"). iIntros "!> !#". setoid_rewrite uninit0_own.
+    iSplit; iIntros; done.
+  Qed.
   Next Obligation. intros. by apply ty_shr_mono. Qed.
 
   Global Instance uninit_wf n : TyWf (uninit n) :=
@@ -33,22 +52,32 @@ Section uninit.
 
   Global Instance uninit_copy n : Copy (uninit n).
   Proof.
-    destruct (product_copy (replicate n uninit_1)) as [A B].
-      by apply Forall_replicate, _.
-    rewrite uninit0_sz in B. by split.
+    assert (Copy (uninit0 n)) as [A B].
+    { apply product_copy. by apply Forall_replicate, _. }
+    split; first by apply _.
+    rewrite uninit0_sz in B. setoid_rewrite uninit0_own in B. done.
   Qed.
 
   Global Instance uninit_send n : Send (uninit n).
-  Proof. apply product_send, Forall_replicate, _. Qed.
+  Proof. iIntros (???) "?". done. Qed.
 
   Global Instance uninit_sync n : Sync (uninit n).
   Proof. apply product_sync, Forall_replicate, _. Qed.
 
+  (* Unfolding lemma, kep only for backwards compatibility. *)
+  Lemma uninit_own n tid vl :
+    (uninit n).(ty_own) tid vl ⊣⊢ ⌜length vl = n⌝.
+  Proof. done. Qed.
+
   Lemma uninit_uninit0_eqtype E L n :
     eqtype E L (uninit0 n) (uninit n).
-  Proof. apply equiv_eqtype; constructor=>//=. apply uninit0_sz. Qed.
+  Proof.
+    apply equiv_eqtype; constructor=>//=.
+    - apply uninit0_sz.
+    - iIntros (??). rewrite uninit0_own. done.
+  Qed.
 
-  Lemma uninit_product_subtype_cons {E L} (n : nat) ty tyl :
+  Lemma uninit_product_subtype_cons_r {E L} (n : nat) ty tyl :
     ty.(ty_size) ≤ n →
     subtype E L (uninit ty.(ty_size)) ty →
     subtype E L (uninit (n-ty.(ty_size))) (Π tyl) →
@@ -58,7 +87,7 @@ Section uninit.
     rewrite (le_plus_minus ty.(ty_size) n) // replicate_plus
            -(prod_flatten_r _ _ [_]) /= -prod_app. repeat (done || f_equiv).
   Qed.
-  Lemma uninit_product_subtype_cons' {E L} (n : nat) ty tyl :
+  Lemma uninit_product_subtype_cons_l {E L} (n : nat) ty tyl :
     ty.(ty_size) ≤ n →
     subtype E L ty (uninit ty.(ty_size)) →
     subtype E L (Π tyl) (uninit (n-ty.(ty_size))) →
@@ -68,22 +97,22 @@ Section uninit.
     rewrite (le_plus_minus ty.(ty_size) n) // replicate_plus
            -(prod_flatten_r _ _ [_]) /= -prod_app. repeat (done || f_equiv).
   Qed.
-  Lemma uninit_product_eqtype_cons {E L} (n : nat) ty tyl :
+  Lemma uninit_product_eqtype_cons_r {E L} (n : nat) ty tyl :
     ty.(ty_size) ≤ n →
     eqtype E L (uninit ty.(ty_size)) ty →
     eqtype E L (uninit (n-ty.(ty_size))) (Π tyl) →
     eqtype E L (uninit n) (Π(ty :: tyl)).
   Proof.
     intros ? [] []. split.
-    - by apply uninit_product_subtype_cons.
-    - by apply uninit_product_subtype_cons'.
+    - by apply uninit_product_subtype_cons_r.
+    - by apply uninit_product_subtype_cons_l.
   Qed.
-  Lemma uninit_product_eqtype_cons' {E L} (n : nat) ty tyl :
+  Lemma uninit_product_eqtype_cons_l {E L} (n : nat) ty tyl :
     ty.(ty_size) ≤ n →
     eqtype E L ty (uninit ty.(ty_size)) →
     eqtype E L (Π tyl) (uninit (n-ty.(ty_size))) →
     eqtype E L (Π(ty :: tyl)) (uninit n).
-  Proof. symmetry. by apply uninit_product_eqtype_cons. Qed.
+  Proof. symmetry. by apply uninit_product_eqtype_cons_r. Qed.
 
   Lemma uninit_unit_eqtype E L n :
     n = 0%nat →
@@ -101,21 +130,9 @@ Section uninit.
     n = 0%nat →
     subtype E L unit (uninit n).
   Proof. rewrite -uninit_uninit0_eqtype=>->//. Qed.
-
-  Lemma uninit_own n tid vl :
-    (uninit n).(ty_own) tid vl ⊣⊢ ⌜length vl = n⌝.
-  Proof.
-    iSplit.
-    - rewrite ty_size_eq. auto.
-    - iInduction vl as [|v vl] "IH" forall (n).
-      + iIntros "%". by destruct n; simpl.
-      + iIntros (Heq). destruct n; first done. simpl.
-        iExists [v], vl. iSplit; first done. iSplit; first done.
-        unfold uninit0, product. iApply "IH". by inversion Heq.
-  Qed.
 End uninit.
 
-Hint Resolve uninit_product_eqtype_cons uninit_product_eqtype_cons'
-             uninit_product_subtype_cons uninit_product_subtype_cons'
+Hint Resolve uninit_product_eqtype_cons_l uninit_product_eqtype_cons_r
+             uninit_product_subtype_cons_l uninit_product_subtype_cons_r
              uninit_unit_eqtype uninit_unit_eqtype'
              uninit_unit_subtype uninit_unit_subtype' : lrust_typing.