diff --git a/theories/typing/examples/get_x.v b/theories/typing/examples/get_x.v
index 75b78efc763e83a6eda0e1a18609ebd4e53b9d21..2787f7dbfa27ee48dec69793da38cbeae364178d 100644
--- a/theories/typing/examples/get_x.v
+++ b/theories/typing/examples/get_x.v
@@ -12,7 +12,10 @@ Section get_x.
 
   Lemma get_x_type :
     typed_instruction_ty [] [] [] get_x
-        (fn (λ α, [☀α])%EL (λ α, [# &uniq{α}Π[int; int]]%T) (λ α, &shr{α} int)%T).
+        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. *)
   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 24c34b29da7f67bc90ba3730e5b57df00f794713..7ddaf2c835a7dfd6e471258076a21b7e5ff1d2ab 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 d1d865bd7796deb9f7aeb006ac75c09049483ac1..0c8315b4b2e3335228cdaa82e4cc09d14a03e0f1 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 (λ _, [#]) (λ _:(), 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 ae5c951bef7e46c5a42cf294a04ac0468156df59..6b92b16001fab42115d2687472eb07ae89715a01 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 (λ α, [☀α])%EL (λ α, [# &uniq{α}Σ[unit; τ]]%T) (λ α, Σ[unit; &uniq{α}τ])%T).
+        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 1a3237202f04687418850848bd8db1558488c849..10579790179d66005b71883f7be086f5d3b666ce 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 ffdb94a7b7302eedc5eb87923e2243a17e726054..48fd570100d5652b158d17bb835e75c95759547e 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 (λ α, [# &uniq{α}box (Π[int; int])]%T) (λ α, &uniq{α} int)%T).
+        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 a14417f97970855e2669958dc80582519dc6a644..a282f6cfbfb108d2ca1dbbd88be13990807433aa 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 (λ _, [# Σ[unit; τ]; τ])%T (λ _:(), τ)).
+        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 4911f96adf310b679209664dd7343efeadc3308e..06de70aa6cd72c4e3cae6330ae0d11bfe180b717 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -65,14 +65,22 @@ Section fn.
   Qed.
 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 ')'" :=
   (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 ')'" :=
+  (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 ')'" :=
   (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 ')'" :=
+  (fn (λ _:(), E%EL) (λ _, Vector.nil) (λ _, R%T))
+  (at level 0, E, R at level 50,
+   format "'fn(' E ';' '→'  R ')'") : lrust_type_scope.
 
 Section typing.
   Context `{typeG Σ}.
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index aa24794b040c2f8fd751d96ca32f80f7c3fac9b9..16be9ec89affe76c7cd7ba68af3e3821fa1265cc 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -80,7 +80,7 @@ Section typing.
 End typing.
 
 Notation typed_instruction_ty E L T1 e ty :=
-  (typed_instruction E L T1 e (λ v : val, [v ◁ ty]%TC)).
+  (typed_instruction E L T1 e (λ v : val, [v ◁ ty%list%T]%TC)).
 
 Section typing_rules.
   Context `{typeG Σ}.
diff --git a/theories/typing/type_context.v b/theories/typing/type_context.v
index b84b52da0ad1209e1b1609aeb51aa82e3f67a440..77a4aa7eecb2fa79804383fcf4d8ceb82d694de0 100644
--- a/theories/typing/type_context.v
+++ b/theories/typing/type_context.v
@@ -17,7 +17,7 @@ Notation tctx := (list tctx_elt).
 Delimit Scope lrust_tctx_scope with TC.
 Bind Scope lrust_tctx_scope with tctx_elt.
 
-Infix "◁" := TCtx_hasty (at level 70) : lrust_tctx_scope.
+Notation "p ◁ ty" := (TCtx_hasty p ty%list%T) (at level 70) : lrust_tctx_scope.
 Notation "p ◁{ κ } ty" := (TCtx_blocked p κ ty)
    (at level 70, format "p  ◁{ κ }  ty") : lrust_tctx_scope.
 Notation "a :: b" := (@cons tctx_elt a%TC b%TC)
diff --git a/theories/typing/unsafe/refcell/refmut_code.v b/theories/typing/unsafe/refcell/refmut_code.v
index 8d29b53cd55a46ed6b5628dfaf585eeec5b05880..76201905a832f1ee385c30fc1ffc7eb121ee4922 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 (fun α => [☀α])%EL (fun α => [# refmut α ty])  (fun α => 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".