diff --git a/_CoqProject b/_CoqProject
index f801938fc374ec3b143822039e72362c3dedfaf6..65799cfc1c5a0f6fab9b2b84cef4518e3b7d9163 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -53,6 +53,7 @@ theories/typing/examples/option_as_mut.v
 theories/typing/examples/unwrap_or.v
 theories/typing/examples/lazy_lft.v
 theories/typing/unsafe/cell.v
+theories/typing/unsafe/spawn.v
 theories/typing/unsafe/refcell/refcell.v
 theories/typing/unsafe/refcell/ref.v
 theories/typing/unsafe/refcell/refmut.v
diff --git a/theories/typing/examples/get_x.v b/theories/typing/examples/get_x.v
index 2787f7dbfa27ee48dec69793da38cbeae364178d..fa618fec2f8993dfdd69fd7acbe5102626e12ce2 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(∀ α, [☀α]; &uniq{α} Π[int; int] → &shr{α} int).
+        (fn(∀ α, [☀α]; &uniq{α} Π[int; int]) → &shr{α} int).
   (* FIXME: The above is pretty-printed with some explicit scope annotations,
      and without using 'typed_instruction_ty'.  I think that's related to
      the list notation that we added to %TC. *)
diff --git a/theories/typing/examples/init_prod.v b/theories/typing/examples/init_prod.v
index 7ddaf2c835a7dfd6e471258076a21b7e5ff1d2ab..5a192f809da6fc3e395cfe399947404dc062f991 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([]; int, int → Π[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 0c8315b4b2e3335228cdaa82e4cc09d14a03e0f1..40179b7d550ba9b9c5a4662b740769a0aef5d86a 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([]; → unit).
+        (fn([]) → 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 6b92b16001fab42115d2687472eb07ae89715a01..376e6cfe9ff6235ef9f0545ea2be59665c88974b 100644
--- a/theories/typing/examples/option_as_mut.v
+++ b/theories/typing/examples/option_as_mut.v
@@ -16,7 +16,7 @@ Section option_as_mut.
 
   Lemma option_as_mut_type Ï„ :
     typed_instruction_ty [] [] [] option_as_mut
-        fn(∀ α, [☀α]; &uniq{α} Σ[unit; τ] → Σ[unit; &uniq{α}τ]).
+        (fn(∀ α, [☀α]; &uniq{α} Σ[unit; τ]) → Σ[unit; &uniq{α}τ]).
   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 10579790179d66005b71883f7be086f5d3b666ce..5497184dae1643ef1c1a5d8e769a791fd261f1e6 100644
--- a/theories/typing/examples/rebor.v
+++ b/theories/typing/examples/rebor.v
@@ -17,7 +17,7 @@ Section rebor.
 
   Lemma rebor_type :
     typed_instruction_ty [] [] [] rebor
-        fn([]; Π[int; int], Π[int; int] → 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 48fd570100d5652b158d17bb835e75c95759547e..f1765799d8cec8d516abc8f2ca0ee11f0c37671a 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(∀ α, [☀α]; &uniq{α}box (Π[int; int]) → &uniq{α} int).
+        (fn(∀ α, [☀α]; &uniq{α}box (Π[int; int])) → &uniq{α} int).
   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 a282f6cfbfb108d2ca1dbbd88be13990807433aa..b6a5e1c1ec21776cea8460604f45b2599cab0a70 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([]; Σ[unit; τ], τ → τ).
+        (fn([]; Σ[unit; τ], τ) → τ).
   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 06de70aa6cd72c4e3cae6330ae0d11bfe180b717..d2ce65cb74ae1be16831276ddecaf9d7f9e7bbc7 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -67,20 +67,22 @@ End fn.
 
 (* TODO: Once we depend on 8.6pl1, extend this to recursive binders so that
    patterns like '(a, b) can be used. *)
-Notation "'fn(∀' x ',' E ';' T1 ',' .. ',' TN '→' R ')'" :=
+Notation "'fn(∀' x ',' E ';' T1 ',' .. ',' TN ')' '→' R" :=
   (fn (λ x, E%EL) (λ x, (Vector.cons T1 .. (Vector.cons TN Vector.nil) ..)%T) (λ x, R%T))
-  (at level 0, E, T1, TN, R at level 50) : lrust_type_scope.
-Notation "'fn(∀' x ',' E ';' '→' R ')'" :=
+  (at level 99, R at level 200,
+   format "'fn(∀' x ','  E ';'  T1 ','  .. ','  TN ')'  '→'  R") : lrust_type_scope.
+Notation "'fn(∀' x ',' E ')' '→' R" :=
   (fn (λ x, E%EL) (λ x, Vector.nil) (λ x, R%T))
-  (at level 0, E, R at level 50) : lrust_type_scope.
-Notation "'fn(' E ';' T1 ',' .. ',' TN '→' R ')'" :=
+  (at level 99, R at level 200,
+   format "'fn(∀' x ','  E ')'  '→'  R") : lrust_type_scope.
+Notation "'fn(' E ';' T1 ',' .. ',' TN ')' '→' R" :=
   (fn (λ _:(), E%EL) (λ _, (Vector.cons T1 .. (Vector.cons TN Vector.nil) ..)%T) (λ _, R%T))
-  (at level 0, E, T1, TN, R at level 50,
-   format "'fn(' E ';'  T1 ','  .. ','  TN  '→'  R ')'") : lrust_type_scope.
-Notation "'fn(' E ';' '→' R ')'" :=
+  (at level 99, R at level 200,
+   format "'fn(' E ';'  T1 ','  .. ','  TN ')'  '→'  R") : lrust_type_scope.
+Notation "'fn(' E ')' '→' R" :=
   (fn (λ _:(), E%EL) (λ _, Vector.nil) (λ _, R%T))
-  (at level 0, E, R at level 50,
-   format "'fn(' E ';' '→'  R ')'") : lrust_type_scope.
+  (at level 99, R at level 200,
+   format "'fn(' E ')'  '→'  R") : lrust_type_scope.
 
 Section typing.
   Context `{typeG Σ}.
diff --git a/theories/typing/soundness.v b/theories/typing/soundness.v
index c6f7e7b479ff4dd7b8eeec482880687a553cdd9c..e5ca263bafce794e3983ccacb2afe70b22b2b9b3 100644
--- a/theories/typing/soundness.v
+++ b/theories/typing/soundness.v
@@ -24,7 +24,7 @@ Section type_soundness.
   Definition exit_cont : val := λ: [<>], #().
 
   Definition main_type `{typeG Σ} :=
-    fn (λ _, []) (λ _, [# ]) (λ _:(), box unit).
+    (fn([]) → unit)%T.
 
   Theorem type_soundness `{typePreG Σ} (main : val) σ t :
     (∀ `{typeG Σ}, typed_instruction_ty [] [] [] main main_type) →
diff --git a/theories/typing/unsafe/cell.v b/theories/typing/unsafe/cell.v
index 2333767d69bb22954f3d08130af4570488dfc7cc..a7b050cfd52b22d93dcb11ecd01d9177d4477ff1 100644
--- a/theories/typing/unsafe/cell.v
+++ b/theories/typing/unsafe/cell.v
@@ -81,7 +81,7 @@ Section typing.
 
   Lemma cell_new_type ty :
     typed_instruction_ty [] [] [] cell_new
-        fn([]; ty → cell ty).
+        (fn([]; ty) → cell ty).
   Proof.
     apply type_fn; [apply _..|]. move=>/= _ ret arg. inv_vec arg=>x. simpl_subst.
     eapply (type_jump [_]); first solve_typing.
@@ -93,7 +93,7 @@ Section typing.
 
   Lemma cell_into_inner_type ty :
     typed_instruction_ty [] [] [] cell_into_inner
-        fn([]; cell ty → ty).
+        (fn([]; cell ty) → ty).
   Proof.
     apply type_fn; [apply _..|]. move=>/= _ ret arg. inv_vec arg=>x. simpl_subst.
     eapply (type_jump [_]); first solve_typing.
@@ -105,7 +105,7 @@ Section typing.
 
   Lemma cell_get_mut_type ty :
     typed_instruction_ty [] [] [] cell_get_mut
-      fn(∀ α, [☀α]; &uniq{α} (cell ty) → &uniq{α} ty).
+      (fn(∀ α, [☀α]; &uniq{α} (cell ty)) → &uniq{α} ty).
   Proof.
     apply type_fn; [apply _..|]. move=>/= α ret arg. inv_vec arg=>x. simpl_subst.
     eapply (type_jump [_]). solve_typing. rewrite /tctx_incl /=.
@@ -122,7 +122,7 @@ Section typing.
 
   Lemma cell_get_type `(!Copy ty) :
     typed_instruction_ty [] [] [] (cell_get ty)
-        fn(∀ α, [☀α]; &shr{α} (cell ty) → ty).
+        (fn(∀ α, [☀α]; &shr{α} (cell ty)) → 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.
@@ -142,7 +142,7 @@ Section typing.
 
   Lemma cell_set_type ty :
     typed_instruction_ty [] [] [] (cell_set ty)
-        fn(∀ α, [☀α]; &shr{α} cell ty, ty → unit).
+        (fn(∀ α, [☀α]; &shr{α} cell ty, ty) → 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|].
diff --git a/theories/typing/unsafe/refcell/refmut_code.v b/theories/typing/unsafe/refcell/refmut_code.v
index 82e5603174390392a005c4bfedb9955624c2f752..e3e528509b0b42e3d578f1975ed676a98760d888 100644
--- a/theories/typing/unsafe/refcell/refmut_code.v
+++ b/theories/typing/unsafe/refcell/refmut_code.v
@@ -122,7 +122,7 @@ Section refmut_functions.
 
   Lemma refmut_drop_type ty :
     typed_instruction_ty [] [] [] refmut_drop
-      fn(∀ α, [☀α]; refmut α ty → unit).
+      (fn(∀ α, [☀α]; refmut α ty) → unit).
   Proof.
     apply type_fn; [apply _..|]. move=>/= α ret arg. inv_vec arg=>x. simpl_subst.
     iIntros "!# * #LFT Hna Hα HL Hk Hx".
diff --git a/theories/typing/unsafe/spawn.v b/theories/typing/unsafe/spawn.v
new file mode 100644
index 0000000000000000000000000000000000000000..20eac315935c5a4518c3a5f10c4def964f2476d9
--- /dev/null
+++ b/theories/typing/unsafe/spawn.v
@@ -0,0 +1,55 @@
+From iris.proofmode Require Import tactics.
+From iris.base_logic Require Import big_op.
+From lrust.typing Require Export type.
+From lrust.typing Require Import typing.
+Set Default Proof Using "Type".
+
+Section spawn.
+  Context `{typeG Σ}.
+
+  Definition thread_cont : val := λ: [<>], #().
+
+  Definition spawn : val :=
+    funrec: <> ["f"; "env"] :=
+      let: "f'" := !"f" in
+      Fork (call: "f'" ["env":expr] → thread_cont);;
+      let: "r" := new [ #0 ] in
+      delete [ #1; "f"];; "return" ["r"].
+
+  Lemma spawn_type `(!Send envty) :
+    typed_instruction_ty [] [] [] spawn
+        (fn([]; fn([] ; envty) → unit, envty) → unit).
+  Proof. (* FIXME: typed_instruction_ty is not used for printing. *)
+    apply type_fn; [apply _..|]=>_ ret /= arg. inv_vec arg=>f env. simpl_subst.
+    eapply type_deref; [solve_typing..|exact: read_own_move|done|].
+    move=>f'. simpl_subst.
+    eapply type_let with (T1 := [f' ◁ _; env ◁ _]%TC)
+                         (T2 := λ _, []); try solve_typing; [|].
+    { (* The core of the proof: showing that Forking is safe. *)
+      iAlways. iIntros (tid qE) "#LFT $ $ $".
+      rewrite tctx_interp_cons tctx_interp_singleton.
+      iIntros "[Hf' Henv]". iApply (wp_fork with "[-]"); last first.
+      { rewrite tctx_interp_nil. auto. }
+      iNext. iMod na_alloc as (tid') "Htl".
+      iApply (type_call' [] [] (λ _:(), []) [] f' [env:expr]
+              (λ _, [# envty]) (λ _, unit) thread_cont () $! _ 1%Qp with "LFT Htl").
+      - apply elctx_sat_nil.
+      - rewrite /elctx_interp big_sepL_nil. done.
+      - rewrite /llctx_interp big_sepL_nil. done.
+      - rewrite /cctx_interp. iIntros "_ * Hin".
+        iDestruct "Hin" as %Hin%elem_of_list_singleton. subst x.
+        rewrite /cctx_elt_interp. iIntros "* ???". inv_vec args=>arg /=.
+        wp_seq. auto.
+      - rewrite tctx_interp_cons tctx_interp_singleton. iSplitL "Hf'".
+        + rewrite !tctx_hasty_val.
+          (* FIXME: The following should work, but does not. TC inference is doing sth. wrong.
+             iApply (send_change_tid with "Hf'"). *)
+          iApply @send_change_tid. done.
+        + rewrite !tctx_hasty_val. iApply @send_change_tid. done. }
+    move=>v. simpl_subst. clear v.
+    eapply type_new; [solve_typing..|].
+    intros r. simpl_subst.
+    eapply type_delete; [solve_typing..|].
+    eapply (type_jump [_]); solve_typing.
+  Qed.
+End spawn.