diff --git a/theories/typing/type.v b/theories/typing/type.v
index 5a8ba446351d633333ed21ff674f0c6beb9d8196..86459792ec338a3c416864e91d748bfbf26560e8 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -353,6 +353,7 @@ Section subtyping.
 
   Definition subtype (ty1 ty2 : type) : Prop :=
     lft_ctx -∗ elctx_interp_0 E -∗ ⌜llctx_interp_0 L⌝ -∗ type_incl ty1 ty2.
+  (* TODO RJ: I'd really like to get rid of this definition. *)
   Definition ctx_eq {A} (x1 x2 : A) : Prop :=
     lft_ctx -∗ elctx_interp_0 E -∗ ⌜llctx_interp_0 L⌝ -∗ ⌜x1 = x2⌝.
 
diff --git a/theories/typing/unsafe/spawn.v b/theories/typing/unsafe/spawn.v
index b140d744555bd7dd963a7ff2da2c1769ddb5b3b3..aa79c626e971be535b336173b097980c1b8ba997 100644
--- a/theories/typing/unsafe/spawn.v
+++ b/theories/typing/unsafe/spawn.v
@@ -32,17 +32,22 @@ Section join_handle.
     iIntros (?) "* _ _ _". auto.
   Qed.
 
+  Lemma join_handle_subtype ty1 ty2 :
+    type_incl ty1 ty2 -∗ type_incl (join_handle ty1) (join_handle ty2).
+  Proof.
+    iIntros "#Hincl". iSplit; first done. iSplit; iAlways.
+    - 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'"). done.
+    - iIntros "* _". auto.
+  Qed.
+
   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.
+    iIntros (ty1 ty2 Hsub) "#? #? #?". iApply join_handle_subtype.
+    iApply Hsub; done.
   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.