diff --git a/theories/typing/own.v b/theories/typing/own.v
index ae40afd3c06a74b7f7b96ad51ffb42d6b800258e..af0840fcd55852f17ce5aa6ab87e4407df21bb61 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -98,24 +98,27 @@ Section own.
     by iApply (ty.(ty_shr_mono) with "LFT Hκ").
   Qed.
 
-  Global Instance own_mono E L :
-    Proper (ctx_eq E L ==> subtype E L ==> subtype E L) own_ptr.
+  Lemma own_type_incl n ty1 ty2 :
+    type_incl ty1 ty2 -∗ type_incl (own_ptr n ty1) (own_ptr n ty2).
   Proof.
-    intros n1 n2 Hn12 ty1 ty2 Hincl. iIntros. iSplit; first done.
-    iDestruct (Hincl with "[] [] []") as "(_ & #Ho & #Hs)"; [done..|clear Hincl].
-    iSplit; iAlways.
+    iIntros "(#Hsz & #Ho & #Hs)". iSplit; first done. iSplit; iAlways.
     - iIntros (?[|[[| |]|][]]) "H"; try iDestruct "H" as "[]". simpl.
       iDestruct "H" as "[Hmt H†]". 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 %<-.
-      iDestruct (Hn12 with "[] [] []") as %->; [done..|]. iFrame.
-      iExists _. by iFrame.
+      iDestruct ("Ho" with "Hown") as "Hown". iDestruct ("Hsz") as %<-.
+      iFrame. iExists _. 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.
+
+  Global Instance own_mono E L :
+    Proper (ctx_eq E L ==> subtype E L ==> subtype E L) own_ptr.
+  Proof.
+    intros n1 n2 Hn12 ty1 ty2 Hincl. iIntros.
+    iDestruct (Hn12 with "[] [] []") as %->; [done..|].
+    iApply own_type_incl. iApply Hincl; done.
+  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).
diff --git a/theories/typing/unsafe/spawn.v b/theories/typing/unsafe/spawn.v
index faebd070b4f08fdf32481369c84e055f5477e1fd..b140d744555bd7dd963a7ff2da2c1769ddb5b3b3 100644
--- a/theories/typing/unsafe/spawn.v
+++ b/theories/typing/unsafe/spawn.v
@@ -17,7 +17,8 @@ Section join_handle.
     {| ty_size := 1;
        ty_own tid vl :=
          match vl return _ with
-         | [ #(LitLoc l) ] => join_handle spawnN l (join_inv ty tid)
+         | [ #(LitLoc l) ] =>
+           ∃ ty', type_incl ty' ty ∗ join_handle spawnN l (join_inv ty' tid)
          | _ => False
          end%I;
        ty_shr κ tid l := True%I |}.
@@ -31,15 +32,27 @@ Section join_handle.
     iIntros (?) "* _ _ _". auto.
   Qed.
 
-  (* TODO: figure out whether Rust considers this a pointer type,
-     and whether it allows subtyping. *)
+  Global Instance join_handle_mono E L :
+    Proper (subtype E L ==> subtype E L) join_handle.
+  Proof.
+    iIntros (ty1 ty2 Hsub) "#? #? #?". iSplit; last iSplit; first done.
+    - iIntros "!# * Hvl". destruct vl as [|[[|vl|]|] [|]]; try by iDestruct "Hvl" as "[]".
+      iDestruct "Hvl" as (ty) "[Hincl ?]". iExists ty. iFrame.
+      iApply (type_incl_trans with "Hincl").
+      iDestruct (Hsub with "[] [] []") as "$"; done.
+    - iIntros "!# * _". auto.
+  Qed.
+
+  Global Instance join_handle_proper E L :
+    Proper (eqtype E L ==> eqtype E L) join_handle.
+  Proof. intros ??[]. by split; apply join_handle_mono. Qed.
+
+  (* TODO: Show that the type is contractive. *)
 End join_handle.
 
 Section spawn.
   Context `{!typeG Σ, !spawnG Σ}.
 
-  Definition thread_cont : val := λ: [<>], #().
-
   Definition spawn : val :=
     funrec: <> ["f"; "env"] :=
       let: "f'" := !"f" in
@@ -62,7 +75,8 @@ Section spawn.
       iAlways. iIntros (tid qE) "#LFT $ $ $".
       rewrite tctx_interp_cons tctx_interp_singleton.
       iIntros "[Hf' Henv]". iApply (spawn_spec _ (join_inv retty tid) with "[-]"); first solve_to_val; last first; last simpl_subst.
-      { iIntros "!> *". rewrite tctx_interp_singleton tctx_hasty_val. auto. }
+      { iIntros "!> *". rewrite tctx_interp_singleton tctx_hasty_val.
+        iIntros "?". iExists retty. iFrame. iApply type_incl_refl. }
       iIntros (c) "Hfin". iMod na_alloc as (tid') "Htl". wp_let. wp_let.
       (* FIXME this is horrible. *)
       assert (Hcall := type_call' [] [] (λ _:(), []) [] f' [env:expr]
@@ -107,8 +121,12 @@ Section spawn.
     { iAlways. iIntros (tid qE) "#LFT $ $ $".
       rewrite tctx_interp_singleton tctx_hasty_val. iIntros "Hc'".
       destruct c' as [[|c'|]|]; try by iDestruct "Hc'" as "[]".
+      iDestruct "Hc'" as (ty') "[#Hsub Hc']".
       iApply (join_spec with "Hc'"). iIntros "!> * Hret".
-      rewrite tctx_interp_singleton tctx_hasty_val. auto. }
+      rewrite tctx_interp_singleton tctx_hasty_val.
+      iPoseProof "Hsub" as "Hsz". iDestruct "Hsz" as "[% _]".
+      iDestruct (own_type_incl with "Hsub") as "(_ & Hincl & _)".
+      iApply "Hincl". rewrite -H. done. }
     move=>r; simpl_subst.
     eapply type_delete; [solve_typing..|].
     eapply (type_jump [_]); solve_typing.