diff --git a/theories/typing/examples/get_x.v b/theories/typing/examples/get_x.v
index 54577cbf719a740aa5a5ae9010336ac219575041..75b78efc763e83a6eda0e1a18609ebd4e53b9d21 100644
--- a/theories/typing/examples/get_x.v
+++ b/theories/typing/examples/get_x.v
@@ -12,7 +12,7 @@ Section get_x.
 
   Lemma get_x_type :
     typed_instruction_ty [] [] [] get_x
-        (fn (λ α, [☀α])%EL (λ α, [# box (&uniq{α}Π[int; int])]) (λ α, box (&shr{α} int))).
+        (fn (λ α, [☀α])%EL (λ α, [# &uniq{α}Π[int; int]]%T) (λ α, &shr{α} int)%T).
   Proof.
     apply type_fn; try apply _. move=> /= α ret p. inv_vec p=>p. simpl_subst.
     eapply type_deref; [solve_typing..|by apply read_own_move|done|].
diff --git a/theories/typing/examples/init_prod.v b/theories/typing/examples/init_prod.v
index 8893096ace2ede3ecf2789f100cf01ece7eab906..24c34b29da7f67bc90ba3730e5b57df00f794713 100644
--- a/theories/typing/examples/init_prod.v
+++ b/theories/typing/examples/init_prod.v
@@ -13,7 +13,7 @@ Section init_prod.
 
   Lemma init_prod_type :
     typed_instruction_ty [] [] [] init_prod
-        (fn (λ _, []) (λ _, [# box int; box int]) (λ (_ : ()), box (Π[int;int]))).
+        (fn (λ _, []) (λ _, [# int; int]) (λ (_ : ()), Π[int;int])).
   Proof.
     apply type_fn; try apply _. move=> /= [] ret p. inv_vec p=>x y. simpl_subst.
     eapply type_deref; [solve_typing..|apply read_own_move|done|]=>x'. simpl_subst.
diff --git a/theories/typing/examples/lazy_lft.v b/theories/typing/examples/lazy_lft.v
index aa147026c2c51b4ab7cf84e5213ca659a20c68df..d1d865bd7796deb9f7aeb006ac75c09049483ac1 100644
--- a/theories/typing/examples/lazy_lft.v
+++ b/theories/typing/examples/lazy_lft.v
@@ -18,7 +18,7 @@ Section lazy_lft.
 
   Lemma lazy_lft_type :
     typed_instruction_ty [] [] [] lazy_lft
-        (fn (λ _, [])%EL (λ _, [#]) (λ _:(), box unit)).
+        (fn (λ _, [])%EL (λ _, [#]) (λ _:(), unit)).
   Proof.
     apply type_fn; try apply _. move=> /= [] ret p. inv_vec p. simpl_subst.
     eapply (type_newlft []); [solve_typing|]=>α.
diff --git a/theories/typing/examples/option_as_mut.v b/theories/typing/examples/option_as_mut.v
index 93fac9532f3118ce990aa12437d60775f9ac3a5a..38df7ab70807801746914a6596dfeb09874d8c14 100644
--- a/theories/typing/examples/option_as_mut.v
+++ b/theories/typing/examples/option_as_mut.v
@@ -14,7 +14,7 @@ Section option_as_mut.
 
   Lemma option_as_mut_type Ï„ :
     typed_instruction_ty [] [] [] option_as_mut
-        (fn (λ α, [☀α])%EL (λ α, [# box (&uniq{α}Σ[unit; τ])]) (λ α, box (Σ[unit; &uniq{α}τ]))).
+        (fn (λ α, [☀α])%EL (λ α, [# &uniq{α}Σ[unit; τ]]%T) (λ α, Σ[unit; &uniq{α}τ])%T).
   Proof.
     apply type_fn; try apply _. move=> /= α ret p. inv_vec p=>o. simpl_subst.
     eapply (type_cont [_] [] (λ r, [o ◁ _; r!!!0 ◁ _])%TC) ; [solve_typing..| |].
diff --git a/theories/typing/examples/rebor.v b/theories/typing/examples/rebor.v
index a30f43cb7dff0e744797804ba8e3c5a53f72a9ed..1a3237202f04687418850848bd8db1558488c849 100644
--- a/theories/typing/examples/rebor.v
+++ b/theories/typing/examples/rebor.v
@@ -17,8 +17,7 @@ Section rebor.
 
   Lemma rebor_type :
     typed_instruction_ty [] [] [] rebor
-        (fn (λ _, []) (λ _, [# box (Π[int; int]); box (Π[int; int])])
-            (λ (_ : ()), box int)).
+        (fn (λ _, []) (λ _, [# Π[int; int]; Π[int; int]]) (λ (_ : ()), int)).
   Proof.
     apply type_fn; try apply _. move=> /= [] ret p. inv_vec p=>t1 t2. simpl_subst.
     eapply (type_newlft []). apply _. move=> α.
diff --git a/theories/typing/examples/unbox.v b/theories/typing/examples/unbox.v
index 3f9b02b4cd7866ba6e1175c545ac8378910a690e..ffdb94a7b7302eedc5eb87923e2243a17e726054 100644
--- a/theories/typing/examples/unbox.v
+++ b/theories/typing/examples/unbox.v
@@ -12,7 +12,7 @@ Section unbox.
 
   Lemma ubox_type :
     typed_instruction_ty [] [] [] unbox
-        (fn (λ α, [☀α])%EL (λ α, [# box (&uniq{α}box (Π[int; int]))]) (λ α, box (&uniq{α} int))).
+        (fn (λ α, [☀α])%EL (λ α, [# &uniq{α}box (Π[int; int])]%T) (λ α, &uniq{α} int)%T).
   Proof.
     apply type_fn; try apply _. move=> /= α ret b. inv_vec b=>b. simpl_subst.
     eapply type_deref; [solve_typing..|by apply read_own_move|done|].
diff --git a/theories/typing/examples/unwrap_or.v b/theories/typing/examples/unwrap_or.v
index fabb11e02fb64f03ce5c93d1fb41b1a50fbbaca1..a14417f97970855e2669958dc80582519dc6a644 100644
--- a/theories/typing/examples/unwrap_or.v
+++ b/theories/typing/examples/unwrap_or.v
@@ -13,7 +13,7 @@ Section unwrap_or.
 
   Lemma unwrap_or_type Ï„ :
     typed_instruction_ty [] [] [] (unwrap_or Ï„)
-        (fn (λ _, [])%EL (λ _, [# box (Σ[unit; τ]); box τ]) (λ _:(), box τ)).
+        (fn (λ _, [])%EL (λ _, [# Σ[unit; τ]; τ])%T (λ _:(), τ)).
   Proof.
     apply type_fn; try apply _. move=> /= [] ret p. inv_vec p=>o def. simpl_subst.
     eapply type_case_own; [solve_typing..|]. constructor; last constructor; last constructor.
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 9030e40814bf1afadd8bc2fc9a5d9b974598d89b..3808821a71e05168c776185e1558cb8df8513752 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -2,7 +2,7 @@ From iris.base_logic Require Import big_op.
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import vector.
 From lrust.typing Require Export type.
-From lrust.typing Require Import programs cont.
+From lrust.typing Require Import own programs cont.
 Set Default Proof Using "Type".
 
 Section fn.
@@ -14,8 +14,9 @@ Section fn.
          ⌜vl = [@RecV fb (kb::xb) e H]⌝ ∗ ⌜length xb = n⌝ ∗
          ▷ ∀ (x : A) (k : val) (xl : vec val (length xb)),
             typed_body (E x) []
-                       [k◁cont([], λ v : vec _ 1, [v!!!0 ◁ ty x])]
-                       (zip_with (TCtx_hasty ∘ of_val) xl (tys x))
+                       [k◁cont([], λ v : vec _ 1, [v!!!0 ◁ box (ty x)])]
+                       (zip_with (TCtx_hasty ∘ of_val) xl
+                                 ((λ ty, box ty) <$> (vec_to_list (tys x))))
                        (subst_v (fb::kb::xb) (RecV fb (kb::xb) e:::k:::xl) e))%I |}.
   Next Obligation.
     iIntros (E tys ty tid vl) "H". iDestruct "H" as (fb kb xb e ?) "[% _]". by subst.
@@ -32,11 +33,13 @@ Section fn.
     f_contractive=>tid vl. unfold typed_body.
     do 12 f_equiv. f_contractive. do 18 f_equiv.
     - rewrite !cctx_interp_singleton /=. do 5 f_equiv.
-      rewrite !tctx_interp_singleton /tctx_elt_interp. do 3 f_equiv. apply Hty.
+      rewrite !tctx_interp_singleton /tctx_elt_interp /=. repeat f_equiv. apply Hty.
+      by rewrite (ty_size_proper_d _ _ _ (Hty _)).
     - rewrite /tctx_interp !big_sepL_zip_with /=. do 3 f_equiv.
-      assert (Hprop : ∀ n tid p i, Proper (dist (S n) ==> dist n)
-        (λ (l : list _), ∀ ty, ⌜l !! i = Some ty⌝ → tctx_elt_interp tid (p ◁ ty))%I);
-        last by apply Hprop, Htys.
+      cut (∀ n tid p i, Proper (dist (S n) ==> dist n)
+        (λ (l : list _), ∀ ty, ⌜l !! i = Some ty⌝ → tctx_elt_interp tid (p ◁ ty))%I).
+      { intros Hprop. apply Hprop, list_fmap_ne, Htys. intros ty1 ty2 Hty12.
+        rewrite (ty_size_proper_d _ _ _ Hty12). by rewrite Hty12. }
       clear. intros n tid p i x y. rewrite list_dist_lookup=>Hxy.
       specialize (Hxy i). destruct (x !! i) as [tyx|], (y !! i) as [tyy|];
         inversion_clear Hxy; last done.
@@ -86,7 +89,9 @@ Section typing.
       { by apply elem_of_list_singleton. }
       rewrite /tctx_interp !big_sepL_singleton /=.
       iDestruct "HT" as (v) "[HP Hown]". iExists v. iFrame "HP".
-      iDestruct (Hty x with "LFT [HE0 HEp] HL0") as "(_ & #Hty & _)".
+      assert (Hst : subtype (E0 ++ E x) L0 (box (ty x)) (box (ty' x)))
+        by by rewrite ->Hty.
+      iDestruct (Hst with "LFT [HE0 HEp] HL0") as "(_ & Hty & _)".
       { rewrite /elctx_interp_0 big_sepL_app. by iSplit. }
       by iApply "Hty".
     - rewrite /tctx_interp
@@ -100,9 +105,11 @@ Section typing.
       iDestruct "Hzip" as %(? & ? & ([? ?] & (? & Hty'1 &
         (? & Hty'2 & [=->->])%bind_Some)%bind_Some & [=->->->])%bind_Some)%bind_Some.
       specialize (Htys x). eapply Forall2_lookup_lr in Htys; try done.
-      iDestruct (Htys with "* [] [] []") as "(_ & #Ho & _)"; [done| |done|].
-      + rewrite /elctx_interp_0 big_sepL_app. by iSplit.
-      + by iApply "Ho".
+      assert (Hst : subtype (E0 ++ E x) L0 (box ty2') (box ty1'))
+        by by rewrite ->Htys.
+      iDestruct (Hst with "* [] [] []") as "(_ & #Ho & _)"; [done| |done|].
+      { rewrite /elctx_interp_0 big_sepL_app. by iSplit. }
+      by iApply "Ho".
   Qed.
 
   Lemma fn_subtype_ty {A n} E0 L0 E (tys1 tys2 : A → vec type n) ty1 ty2 :
@@ -159,19 +166,21 @@ Section typing.
   Lemma type_call' {A} E L E' T p (ps : list path)
                          (tys : A → vec type (length ps)) ty k x :
     elctx_sat E L (E' x) →
-    typed_body E L [k ◁cont(L, λ v : vec _ 1, (v!!!0 ◁ ty x) :: T)]
-               ((p ◁ fn E' tys ty) :: zip_with TCtx_hasty ps (tys x) ++ T)
+    typed_body E L [k ◁cont(L, λ v : vec _ 1, (v!!!0 ◁ box (ty x)) :: T)]
+               ((p ◁ fn E' tys ty) ::
+                zip_with TCtx_hasty ps ((λ ty, box ty) <$> (vec_to_list (tys x))) ++
+                T)
                (call: p ps → k).
   Proof.
     iIntros (HE) "!# * #HEAP #LFT Htl HE HL HC".
     rewrite tctx_interp_cons tctx_interp_app. iIntros "(Hf & Hargs & HT)".
     wp_bind p. iApply (wp_hasty with "Hf"). iIntros (v) "% Hf".
     iApply (wp_app_vec _ _ (_::_) ((λ v, ⌜v = k⌝):::
-               vmap (λ ty (v : val), tctx_elt_interp tid (v ◁ ty)) (tys x))%I
+               vmap (λ ty (v : val), tctx_elt_interp tid (v ◁ box ty)) (tys x))%I
             with "* [Hargs]"); first wp_done.
     - rewrite /= big_sepL_cons. iSplitR "Hargs"; first by iApply wp_value'.
       clear dependent ty k p.
-      rewrite /tctx_interp vec_to_list_map zip_with_fmap_r
+      rewrite /tctx_interp vec_to_list_map !zip_with_fmap_r
               (zip_with_zip (λ e ty, (e, _))) zip_with_zip !big_sepL_fmap.
       iApply (big_sepL_mono' with "Hargs"). iIntros (i [p ty]) "HT/=".
       iApply (wp_hasty with "HT"). setoid_rewrite tctx_hasty_val. iIntros (?) "? $".
@@ -192,7 +201,7 @@ Section typing.
         iSpecialize ("HC" with "* []"); first by (iPureIntro; apply elem_of_list_singleton).
         iApply ("HC" $! args with "Htl HL").
         rewrite tctx_interp_singleton tctx_interp_cons. iFrame.
-      + rewrite /tctx_interp vec_to_list_map zip_with_fmap_r
+      + rewrite /tctx_interp vec_to_list_map !zip_with_fmap_r
                 (zip_with_zip (λ v ty, (v, _))) zip_with_zip !big_sepL_fmap.
         iApply (big_sepL_mono' with "Hvl"). by iIntros (i [v ty']).
   Qed.
@@ -201,9 +210,10 @@ Section typing.
                         (tys : A → vec type (length ps)) ty k :
     (p ◁ fn E' tys ty)%TC ∈ T →
     elctx_sat E L (E' x) →
-    tctx_extract_ctx E L (zip_with TCtx_hasty ps (tys x)) T T' →
+    tctx_extract_ctx E L (zip_with TCtx_hasty ps
+                                   ((λ ty, box ty) <$> vec_to_list (tys x))) T T' →
     (k ◁cont(L, T''))%CC ∈ C →
-    (∀ ret : val, tctx_incl E L ((ret ◁ ty x)::T') (T'' [# ret])) →
+    (∀ ret : val, tctx_incl E L ((ret ◁ box (ty x))::T') (T'' [# ret])) →
     typed_body E L C T (call: p ps → k).
   Proof.
     intros Hfn HE HTT' HC HT'T''.
@@ -219,11 +229,12 @@ Section typing.
     Closed (b :b: []) e → Closed [] p → Forall (Closed []) ps →
     (p ◁ fn E' tys ty)%TC ∈ T →
     elctx_sat E L (E' x) →
-    tctx_extract_ctx E L (zip_with TCtx_hasty ps (tys x)) T T' →
-    (∀ ret : val, typed_body E L C ((ret ◁ ty x)::T') (subst' b ret e)) →
+    tctx_extract_ctx E L (zip_with TCtx_hasty ps
+                                   ((λ ty, box ty) <$> vec_to_list (tys x))) T T' →
+    (∀ ret : val, typed_body E L C ((ret ◁ box (ty x))::T') (subst' b ret e)) →
     typed_body E L C T (letcall: b := p ps in e).
   Proof.
-    intros ?? Hpsc ????. eapply (type_cont [_] _ (λ r, (r!!!0 ◁ ty x) :: T')%TC).
+    intros ?? Hpsc ????. eapply (type_cont [_] _ (λ r, (r!!!0 ◁ box (ty x)) :: T')%TC).
     - (* TODO : make [solve_closed] work here. *)
       eapply is_closed_weaken; first done. set_solver+.
     - (* TODO : make [solve_closed] work here. *)
@@ -249,9 +260,10 @@ Section typing.
         T `{!CopyC T, !SendC T} :
     Closed (fb :b: "return" :b: argsb +b+ []) e →
     (∀ x (f : val) k (args : vec val (length argsb)),
-        typed_body (E' x) [] [k ◁cont([], λ v : vec _ 1, [v!!!0 ◁ ty x])]
+        typed_body (E' x) [] [k ◁cont([], λ v : vec _ 1, [v!!!0 ◁ box (ty x)])]
                    ((f ◁ fn E' tys ty) ::
-                      zip_with (TCtx_hasty ∘ of_val) args (tys x) ++ T)
+                      zip_with (TCtx_hasty ∘ of_val) args
+                               ((λ ty, box ty) <$> vec_to_list (tys x)) ++ T)
                    (subst_v (fb :: BNamed "return" :: argsb) (f ::: k ::: args) e)) →
     typed_instruction_ty E L T (funrec: fb argsb := e) (fn E' tys ty).
   Proof.
@@ -271,8 +283,9 @@ Section typing.
         T `{!CopyC T, !SendC T} :
     Closed ("return" :b: argsb +b+ []) e →
     (∀ x k (args : vec val (length argsb)),
-        typed_body (E' x) [] [k ◁cont([], λ v : vec _ 1, [v!!!0 ◁ ty x])]
-                   (zip_with (TCtx_hasty ∘ of_val) args (tys x) ++ T)
+        typed_body (E' x) [] [k ◁cont([], λ v : vec _ 1, [v!!!0 ◁ box (ty x)])]
+                   (zip_with (TCtx_hasty ∘ of_val) args
+                             ((λ ty, box ty) <$> vec_to_list (tys x)) ++ T)
                    (subst_v (BNamed "return" :: argsb) (k ::: args) e)) →
     typed_instruction_ty E L T (funrec: <> argsb := e) (fn E' tys ty).
   Proof.
diff --git a/theories/typing/own.v b/theories/typing/own.v
index 914a1ba997c89c6cefad6f0f5355acdd151bfd69..f4fe9539535cab1b360e075a4de812445ca2c587 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -95,32 +95,35 @@ Section own.
     by iApply (ty.(ty_shr_mono) with "LFT Hκ").
   Qed.
 
-  Global Instance own_mono E L n :
-    Proper (subtype E L ==> subtype E L) (own_ptr n).
+  Global Instance own_mono E L :
+    Proper (ctx_eq E L ==> subtype E L ==> subtype E L) own_ptr.
   Proof.
-    intros ty1 ty2 Hincl. iIntros. iSplit; first done.
+    intros n1 n2 Hn12 ty1 ty2 Hincl. iIntros. iSplit; first done.
     iDestruct (Hincl with "* [] [] []") as "(_ & #Ho & #Hs)"; [done..|clear Hincl].
     iSplit; iAlways.
     - iIntros (??) "H". iDestruct "H" as (l) "(%&Hmt&H†)". subst.
       iExists _. iSplit. done. iDestruct "Hmt" as (vl') "[Hmt Hown]". iNext.
       iDestruct (ty_size_eq with "Hown") as %<-.
       iDestruct ("Ho" with "* Hown") as "Hown".
-      iDestruct (ty_size_eq with "Hown") as %<-. iFrame.
+      iDestruct (ty_size_eq with "Hown") as %<-.
+      iDestruct (Hn12 with "[] [] []") as %->; [done..|]. iFrame.
       iExists _. by iFrame.
     - iIntros (???) "H". iDestruct "H" as (l') "[Hfb #Hvs]".
       iExists l'. iFrame. iIntros "!#". iIntros (F' q) "% Htok".
       iMod ("Hvs" with "* [%] Htok") as "Hvs'". done. iModIntro. iNext.
       iMod "Hvs'" as "[Hshr $]". iApply ("Hs" with "Hshr").
   Qed.
-  Lemma own_mono' E L n ty1 ty2 :
-    subtype E L ty1 ty2 → subtype E L (own_ptr n ty1) (own_ptr n ty2).
-  Proof. apply own_mono. Qed.
-  Global Instance own_proper E L n :
-    Proper (eqtype E L ==> eqtype E L) (own_ptr n).
-  Proof. intros ?? Heq. split; f_equiv; apply Heq. Qed.
-  Lemma own_proper' E L n ty1 ty2 :
-    eqtype E L ty1 ty2 → eqtype E L (own_ptr n ty1) (own_ptr n ty2).
-  Proof. apply own_proper. Qed.
+  Lemma own_mono' E L n1 n2 ty1 ty2 :
+    ctx_eq E L n1 n2 → subtype E L ty1 ty2 →
+    subtype E L (own_ptr n1 ty1) (own_ptr n2 ty2).
+  Proof. intros. by apply own_mono. Qed.
+  Global Instance own_proper E L :
+    Proper (ctx_eq E L ==> eqtype E L ==> eqtype E L) own_ptr.
+  Proof. intros ?? ??? Heq. split; f_equiv; try done; apply Heq. Qed.
+  Lemma own_proper' E L n1 n2 ty1 ty2 :
+    ctx_eq E L n1 n2 → eqtype E L ty1 ty2 →
+    eqtype E L (own_ptr n1 ty1) (own_ptr n2 ty2).
+  Proof. intros. by apply own_proper. Qed.
 
   Global Instance own_contractive n : Contractive (own_ptr n).
   Proof.
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 979af897b555b8e431be990bae3bf814fd375e9e..e2114448b66ab47b1e954246813d9d26e2961d3a 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -352,15 +352,12 @@ Section subtyping.
   Context (E : elctx) (L : llctx).
 
   Definition subtype (ty1 ty2 : type) : Prop :=
-    lft_ctx -∗ elctx_interp_0 E -∗ ⌜llctx_interp_0 L⌝ -∗
-            type_incl ty1 ty2.
+    lft_ctx -∗ elctx_interp_0 E -∗ ⌜llctx_interp_0 L⌝ -∗ type_incl ty1 ty2.
+  Definition ctx_eq {A} (x1 x2 : A) : Prop :=
+    lft_ctx -∗ elctx_interp_0 E -∗ ⌜llctx_interp_0 L⌝ -∗ ⌜x1 = x2⌝.
 
   Lemma subtype_refl ty : subtype ty ty.
   Proof. iIntros. iApply type_incl_refl. Qed.
-
-  Lemma equiv_subtype ty1 ty2 : ty1 ≡ ty2 → subtype ty1 ty2.
-  Proof. unfold subtype, type_incl=>EQ. setoid_rewrite EQ. apply subtype_refl. Qed.
-
   Global Instance subtype_preorder : PreOrder subtype.
   Proof.
     split; first by intros ?; apply subtype_refl.
@@ -370,6 +367,31 @@ Section subtyping.
     - iApply (H23 with "[] []"); done.
   Qed.
 
+  Lemma ctx_eq_refl {A} (x : A) : ctx_eq x x.
+  Proof. by iIntros "_ _ _". Qed.
+  Global Instance ctx_eq_equivalent {A} : Equivalence (@ctx_eq A).
+  Proof.
+    split.
+    - by iIntros (?) "_ _ _".
+    - iIntros (x y Hxy) "LFT HE HL". by iDestruct (Hxy with "LFT HE HL") as %->.
+    - iIntros (x y z Hxy Hyz) "LFT HE HL".
+      iDestruct (Hxy with "LFT HE HL") as %->. by iApply (Hyz with "LFT HE HL").
+  Qed.
+
+  Lemma equiv_subtype ty1 ty2 : ty1 ≡ ty2 → subtype ty1 ty2.
+  Proof. unfold subtype, type_incl=>EQ. setoid_rewrite EQ. apply subtype_refl. Qed.
+
+  Global Instance ty_size_proper : Proper (subtype ==> ctx_eq) ty_size.
+  Proof. iIntros (?? Hst) "LFT HE HL". iDestruct (Hst with "LFT HE HL") as "[$ ?]". Qed.
+  Global Instance ty_size_proper_flip : Proper (flip subtype ==> ctx_eq) ty_size.
+  Proof. by intros ?? ->. Qed.
+  Lemma ty_size_proper' ty1 ty2 :
+    subtype ty1 ty2 → ctx_eq (ty_size ty1) (ty_size ty2).
+  Proof. apply ty_size_proper. Qed.
+  Lemma ty_size_proper_flip' ty1 ty2 :
+    subtype ty2 ty1 → ctx_eq (ty_size ty1) (ty_size ty2).
+  Proof. apply ty_size_proper_flip. Qed.
+
   (* TODO: The prelude should have a symmetric closure. *)
   Definition eqtype (ty1 ty2 : type) : Prop :=
     subtype ty1 ty2 ∧ subtype ty2 ty1.
@@ -417,6 +439,9 @@ Section subtyping.
     - intros ??? H1 H2. split; etrans; (apply H1 || apply H2).
   Qed.
 
+  Global Instance ty_size_proper_eq : Proper (eqtype ==> ctx_eq) ty_size.
+  Proof. by intros ?? [-> _]. Qed.
+
   Lemma subtype_simple_type (st1 st2 : simple_type) :
     (∀ tid vl, lft_ctx -∗ elctx_interp_0 E -∗ ⌜llctx_interp_0 L⌝ -∗
                  st1.(st_own) tid vl -∗ st2.(st_own) tid vl) →
@@ -446,5 +471,6 @@ Section weakening.
   Qed.
 End weakening.
 
-Hint Resolve subtype_refl eqtype_refl : lrust_typing.
-Hint Opaque subtype eqtype : lrust_typing.
\ No newline at end of file
+Hint Resolve subtype_refl eqtype_refl ctx_eq_refl ty_size_proper'
+             ty_size_proper_flip': lrust_typing.
+Hint Opaque ctx_eq subtype eqtype : lrust_typing.
\ No newline at end of file
diff --git a/theories/typing/unsafe/cell.v b/theories/typing/unsafe/cell.v
index 65e9def8e3a926a67b35033512d7f5643fbc3f65..679a50a83a7f08d52d8ee7fca595e4289a389c4b 100644
--- a/theories/typing/unsafe/cell.v
+++ b/theories/typing/unsafe/cell.v
@@ -87,7 +87,7 @@ Section typing.
 
   Lemma cell_new_type ty :
     typed_instruction_ty [] [] [] cell_new
-        (fn (λ _, [])%EL (λ _, [# box ty]) (λ _:(), box (cell ty))).
+        (fn (λ _, [])%EL (λ _, [# ty]) (λ _:(), cell ty)).
   Proof.
     apply type_fn; [apply _..|]. move=>/= _ ret arg. inv_vec arg=>x. simpl_subst.
     eapply (type_jump [_]); first solve_typing.
@@ -100,7 +100,7 @@ Section typing.
 
   Lemma cell_into_inner_type ty :
     typed_instruction_ty [] [] [] cell_into_inner
-        (fn (λ _, [])%EL (λ _, [# box (cell ty)]) (λ _:(), box ty)).
+        (fn (λ _, [])%EL (λ _, [# cell ty]) (λ _:(), ty)).
   Proof.
     apply type_fn; [apply _..|]. move=>/= _ ret arg. inv_vec arg=>x. simpl_subst.
     eapply (type_jump [_]); first solve_typing.
@@ -116,7 +116,7 @@ Section typing.
 
   Lemma cell_get_type `(!Copy ty) :
     typed_instruction_ty [] [] [] (cell_get ty)
-        (fn (λ α, [☀α])%EL (λ α, [# box (&shr{α} (cell ty))])%T (λ _, box ty)).
+        (fn (λ α, [☀α])%EL (λ α, [# &shr{α} (cell ty)])%T (λ _, ty)).
   Proof.
     apply type_fn; [apply _..|]. move=>/= α ret arg. inv_vec arg=>x. simpl_subst.
     eapply type_deref; [solve_typing..|apply read_own_move|done|]=>x'. simpl_subst.
@@ -136,8 +136,7 @@ Section typing.
 
   Lemma cell_set_type ty :
     typed_instruction_ty [] [] [] (cell_set ty)
-        (fn (λ α, [☀α])%EL (λ α, [# box (&shr{α} cell ty); box ty])
-            (λ α, box unit)).
+        (fn (λ α, [☀α])%EL (λ α, [# &shr{α} cell ty; ty]%T) (λ α, unit)).
   Proof.
     apply type_fn; try apply _. move=> /= α ret arg. inv_vec arg=>c x. simpl_subst.
     eapply type_deref; [solve_typing..|by apply read_own_move|done|].
@@ -180,8 +179,7 @@ Section typing.
 
   Lemma cell_get_mut_type `(!Copy ty) :
     typed_instruction_ty [] [] [] cell_get_mut
-      (fn (λ α, [☀α])%EL (λ α, [# box (&uniq{α} (cell ty))])%T
-          (λ α, box (&uniq{α} ty))%T).
+      (fn (λ α, [☀α])%EL (λ α, [# &uniq{α} (cell ty)])%T (λ α, &uniq{α} ty)%T).
   Proof.
     apply type_fn; [apply _..|]. move=>/= α ret arg. inv_vec arg=>x. simpl_subst.
     eapply (type_jump [_]). solve_typing. rewrite /tctx_incl /=.