diff --git a/_CoqProject b/_CoqProject
index 6f953fda74213e58bc9ba18c7a5410584c446712..13d7b219355d675b4293f0e0530a1950503c8f88 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -42,3 +42,4 @@ theories/typing/borrow.v
 theories/typing/cont.v
 theories/typing/fixpoint.v
 theories/typing/type_sum.v
+theories/typing/tests/get_x.v
diff --git a/theories/lang/new_delete.v b/theories/lang/new_delete.v
index 5c6c407c6ec2a980c0887d089c14d8ffda92bb0d..fa541f0f4eccd22afc97e422103213641772a8ee 100644
--- a/theories/lang/new_delete.v
+++ b/theories/lang/new_delete.v
@@ -45,5 +45,5 @@ Notation "'letalloc:' x := e1 'in' e2" :=
   ((Lam (@cons binder x%E%E%E nil) (x <- e1 ;; e2)) [new [ #1]])%E
   (at level 102, x at level 1, e1, e2 at level 200) : expr_scope.
 Notation "'letalloc:' x :={ n } ! e1 'in' e2" :=
-  ((Lam (@cons binder x%E%E%E nil) (x <⋯ !{n%Z%V}e1 ;; e2)) [new [ #n]%E%E])%E
+  ((Lam (@cons binder x%E%E%E nil) (x <⋯ !{n%Z%V}e1 ;; e2)) [new [ #n]])%E
   (at level 102, x at level 1, e1, e2 at level 200) : expr_scope.
diff --git a/theories/lang/notation.v b/theories/lang/notation.v
index 86ab9ab4e6d5da7ddba3c2af29bb68b189d86ffd..a47399b5d145fdac854bdb8e18f08680fc8f8c12 100644
--- a/theories/lang/notation.v
+++ b/theories/lang/notation.v
@@ -11,6 +11,11 @@ Coercion Var : string >-> expr.
 Coercion BNamed : string >-> binder.
 Notation "<>" := BAnon : lrust_binder_scope.
 
+Notation "[ x ]" := (@cons expr x%E (@nil expr)) : expr_scope.
+Notation "[ x1 ; x2 ; .. ; xn ]" :=
+  (@cons expr x1%E (@cons expr x2%E
+        (..(@cons expr xn%E (@nil expr))..))) : expr_scope.
+
 (* No scope for the values, does not conflict and scope is often not inferred
 properly. *)
 Notation "# l" := (LitV l%Z%V) (at level 8, format "# l").
diff --git a/theories/lang/tactics.v b/theories/lang/tactics.v
index bc8fd23290cc52b373f2533e24de91634b0e7cd4..a622fddae6bdc74629e053f6937d395f8e138820 100644
--- a/theories/lang/tactics.v
+++ b/theories/lang/tactics.v
@@ -200,14 +200,14 @@ Hint Extern 0 (language.atomic _) => solve_atomic : typeclass_instances.
 
 (** Substitution *)
 Ltac simpl_subst :=
-  simpl;
+  unfold subst_v; simpl;
   repeat match goal with
   | |- context [subst ?x ?er ?e] =>
       let er' := W.of_expr er in let e' := W.of_expr e in
       change (subst x er e) with (subst x (W.to_expr er') (W.to_expr e'));
       rewrite <-(W.to_expr_subst x); simpl (* ssr rewrite is slower *)
   end;
-  unfold W.to_expr.
+  unfold W.to_expr; simpl.
 Arguments W.to_expr : simpl never.
 Arguments subst : simpl never.
 
diff --git a/theories/typing/cont_context.v b/theories/typing/cont_context.v
index b77593cc052695d267eefc78d0d3c77075767d12..b3fb8b9529f1a1fc19fb3c130ace79a65cf45899 100644
--- a/theories/typing/cont_context.v
+++ b/theories/typing/cont_context.v
@@ -12,12 +12,13 @@ Section cont_context_def.
   Record cctx_elt : Type :=
     CCtx_iscont { cctxe_k : val; cctxe_L : llctx;
                   cctxe_n : nat; cctxe_T : vec val cctxe_n → tctx }.
-  Definition cctx := list cctx_elt.
 End cont_context_def.
 Add Printing Constructor cctx_elt.
 
+Notation cctx := (list cctx_elt).
+
 Delimit Scope lrust_cctx_scope with CC.
-Bind Scope lrust_cctx_scope with cctx cctx_elt.
+Bind Scope lrust_cctx_scope with cctx_elt.
 
 Notation "k ◁cont( L , T )" := (CCtx_iscont k L _ T%TC)
   (at level 70, format "k  ◁cont( L ,  T )") : lrust_cctx_scope.
@@ -37,6 +38,7 @@ Section cont_context.
          WP k (of_val <$> (args : list _)) {{ _, cont_postcondition }})%I.
   Definition cctx_interp (tid : thread_id) (C : cctx) : iProp Σ :=
     (∀ (x : cctx_elt), ⌜x ∈ C⌝ -∗ cctx_elt_interp tid x)%I.
+  Global Arguments cctx_interp _ _%CC.
 
   Global Instance cctx_interp_permut tid:
     Proper ((≡ₚ) ==> (⊣⊢)) (cctx_interp tid).
@@ -76,7 +78,8 @@ Section cont_context.
 
   Definition cctx_incl (E : elctx) (C1 C2 : cctx): Prop :=
     ∀ tid q, lft_ctx -∗ (elctx_interp E q -∗ cctx_interp tid C1) -∗
-                        (elctx_interp E q -∗ cctx_interp tid C2).
+                       (elctx_interp E q -∗ cctx_interp tid C2).
+  Global Arguments cctx_incl _%EL _%CC _%CC.
 
   Global Instance cctx_incl_preorder E : PreOrder (cctx_incl E).
   Proof.
diff --git a/theories/typing/function.v b/theories/typing/function.v
index a3e30cdcfdfe0d6d3ee06ffe9e9f5e238da61b84..95981845d64b986ec68d9833d2ad51b71ca35a46 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -244,11 +244,11 @@ Section typing.
       eapply type_call'; try done. constructor. done.
   Qed.
 
-  Lemma type_fn {A} E L E' fb kb (argsb : list binder) e
+  Lemma type_rec {A} E L E' fb kb (argsb : list binder) e
         (tys : A → vec type (length argsb)) ty
         T `{!CopyC T, !SendC T} :
     Closed (fb :b: kb :b: argsb +b+ []) e →
-    (∀ x (f : val) k (args : vec val _),
+    (∀ x (f : val) k (args : vec val (length argsb)),
         typed_body (E' x) [] [k ◁cont([], λ v : vec _ 1, [v!!!0 ◁ ty x])]
                    ((f ◁ fn E' tys ty) ::
                       zip_with (TCtx_hasty ∘ of_val) args (tys x) ++ T)
@@ -265,6 +265,20 @@ Section typing.
     rewrite tctx_interp_cons tctx_interp_app. iFrame "HT' IH".
     by iApply sendc_change_tid.
   Qed.
+
+  Lemma type_fn {A} E L E' kb (argsb : list binder) e
+        (tys : A → vec type (length argsb)) ty
+        T `{!CopyC T, !SendC T} :
+    Closed (kb :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)
+                   (subst_v (kb :: argsb) (k ::: args) e)) →
+    typed_instruction_ty E L T (funrec: <> argsb → kb := e) (fn E' tys ty).
+  Proof.
+    intros. apply type_rec; try done. intros. rewrite -typed_body_mono //=.
+    eapply contains_tctx_incl. by constructor.
+  Qed.
 End typing.
 
 Hint Resolve fn_subtype_full : lrust_typing.
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index fb676f682297418b0ba991a1724befe185136490..76e72e949161892315d50aa793dab0b5fb7c3e42 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -6,10 +6,13 @@ From lrust.lifetime Require Import derived borrow frac_borrow.
 Inductive elctx_elt : Type :=
 | ELCtx_Alive (κ : lft)
 | ELCtx_Incl (κ κ' : lft).
-Definition elctx := list elctx_elt.
+Notation elctx := (list elctx_elt).
 
 Delimit Scope lrust_elctx_scope with EL.
-Bind Scope lrust_elctx_scope with elctx elctx_elt.
+(* We need to define [elctx] and [llctx] as notations to make eauto
+   work. But then, Coq is not able to bind them to their
+   notations, so we have to use [Arguments] everywhere. *)
+Bind Scope lrust_elctx_scope with elctx_elt.
 
 Notation "☀ κ" := (ELCtx_Alive κ) (at level 70) : lrust_elctx_scope.
 Infix "⊑" := ELCtx_Incl (at level 70) : lrust_elctx_scope.
@@ -22,10 +25,10 @@ Notation "[ x1 ; x2 ; .. ; xn ]" :=
 Notation "[ x ]" := (@cons elctx_elt x%EL (@nil elctx_elt)) : lrust_elctx_scope.
 
 Definition llctx_elt : Type := lft * list lft.
-Definition llctx := list llctx_elt.
+Notation llctx := (list llctx_elt).
 
 Delimit Scope lrust_llctx_scope with LL.
-Bind Scope lrust_llctx_scope with llctx llctx_elt.
+Bind Scope lrust_llctx_scope with llctx_elt.
 
 Notation "κ ⊑ κl" := (@pair lft (list lft) κ κl) (at level 70) : lrust_llctx_scope.
 
@@ -66,6 +69,7 @@ Section lft_contexts.
 
   Definition elctx_interp (E : elctx) (q : Qp) : iProp Σ :=
     ([∗ list] x ∈ E, elctx_elt_interp x q)%I.
+  Global Arguments elctx_interp _%EL _%Qp.
   Global Instance elctx_interp_fractional E:
     Fractional (elctx_interp E).
   Proof. intros ??. rewrite -big_sepL_sepL. by setoid_rewrite <-fractional. Qed.
@@ -79,6 +83,7 @@ Section lft_contexts.
 
   Definition elctx_interp_0 (E : elctx) : iProp Σ :=
     ([∗ list] x ∈ E, elctx_elt_interp_0 x)%I.
+  Global Arguments elctx_interp_0 _%EL.
   Global Instance elctx_interp_0_persistent E:
     PersistentP (elctx_interp_0 E).
   Proof. apply _. Qed.
@@ -124,6 +129,7 @@ Section lft_contexts.
 
   Definition llctx_interp (L : llctx) (q : Qp) : iProp Σ :=
     ([∗ list] x ∈ L, llctx_elt_interp x q)%I.
+  Global Arguments llctx_interp _%LL _%Qp.
   Global Instance llctx_interp_fractional L:
     Fractional (llctx_interp L).
   Proof. intros ??. rewrite -big_sepL_sepL. by setoid_rewrite <-fractional. Qed.
@@ -137,6 +143,7 @@ Section lft_contexts.
 
   Definition llctx_interp_0 (L : llctx) : Prop :=
     ∀ x, x ∈ L → llctx_elt_interp_0 x.
+  Global Arguments llctx_interp_0 _%LL.
   Lemma llctx_interp_persist L q :
     llctx_interp L q -∗ ⌜llctx_interp_0 L⌝.
   Proof.
@@ -301,7 +308,7 @@ Section lft_contexts.
   Qed.
 
   Lemma elctx_sat_alive E' κ :
-    lctx_lft_alive κ → elctx_sat E' → elctx_sat ((☀κ) :: E').
+    lctx_lft_alive κ → elctx_sat E' → elctx_sat ((☀κ) :: E')%EL.
   Proof.
     iIntros (Hκ HE' qE qL F ?) "[HE1 HE2] [HL1 HL2]".
     iMod (Hκ with "HE1 HL1") as (q) "[Htok Hclose]". done.
@@ -315,7 +322,7 @@ Section lft_contexts.
   Qed.
 
   Lemma elctx_sat_lft_incl E' κ κ' :
-    lctx_lft_incl κ κ' → elctx_sat E' → elctx_sat ((κ ⊑ κ') :: E').
+    lctx_lft_incl κ κ' → elctx_sat E' → elctx_sat ((κ ⊑ κ') :: E')%EL.
   Proof.
     iIntros (Hκκ' HE' qE qL F ?) "HE HL".
     iAssert (κ ⊑ κ')%I with "[#]" as "#Hincl". iApply (Hκκ' with "[HE] [HL]").
@@ -326,6 +333,10 @@ Section lft_contexts.
   Qed.
 End lft_contexts.
 
+Arguments lctx_lft_incl {_ _ _} _%EL _%LL _ _.
+Arguments lctx_lft_eq {_ _ _} _%EL _%LL _ _.
+Arguments lctx_lft_alive {_ _ _} _%EL _%LL _.
+Arguments elctx_sat {_ _ _} _%EL _%LL _%EL.
 
 Section elctx_incl.
   (* External lifetime context inclusion, in a persistent context.
@@ -341,6 +352,7 @@ Section elctx_incl.
     ∀ qE1, elctx_interp E1 qE1 ={F}=∗ ∃ qE2, elctx_interp E2 qE2 ∗
        (elctx_interp E2 qE2 ={F}=∗ elctx_interp E1 qE1).
   Global Instance : RewriteRelation elctx_incl.
+  Arguments elctx_incl _%EL _%EL.
 
   Global Instance elctx_incl_preorder : PreOrder elctx_incl.
   Proof.
@@ -422,9 +434,11 @@ Section elctx_incl.
   Qed.
 End elctx_incl.
 
-Ltac solve_typing := by eauto 100 with lrust_typing.
+Arguments elctx_incl {_ _ _} _%EL _%LL _%EL _%EL.
 
-Hint Constructors Forall Forall2 : lrust_typing.
+Ltac solve_typing := eauto 100 with lrust_typing typeclass_instances || fail.
+
+Hint Constructors Forall Forall2 elem_of_list : lrust_typing.
 Hint Resolve
      lctx_lft_incl_relf lctx_lft_incl_static lctx_lft_incl_local'
      lctx_lft_incl_external'
@@ -433,13 +447,6 @@ Hint Resolve
      elctx_incl_refl elctx_incl_nil elctx_incl_lft_alive elctx_incl_lft_incl
   : lrust_typing.
 
-(* We declare these as hint extern, so that the [B] parameter of elem_of does
-   not have to be [list _] and can be an alias of this. *)
-Hint Extern 0 (@elem_of _ _ (@elem_of_list _) _ (_ :: _)) =>
-  eapply @elem_of_list_here : lrust_typing.
-Hint Extern 1 (@elem_of _ _ (@elem_of_list _) _ (_ :: _)) =>
-  eapply @elem_of_list_further : lrust_typing.
-
 Hint Resolve lctx_lft_alive_external' | 100 : lrust_typing.
 
 Lemma elctx_incl_lft_incl_alive `{invG Σ, lftG Σ} E L E1 E2 κ κ' :
diff --git a/theories/typing/own.v b/theories/typing/own.v
index 393c71b8a98c70972131477e5770f5ee515127a1..a2a94267c8d71ae72a816c93ec8291576fe995a3 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -221,7 +221,7 @@ Section typing.
     ty.(ty_size) = 1%nat →
     Closed [] p → Closed (x :b: []) e →
     tctx_extract_hasty E L p ty T T' →
-    (∀ v, typed_body E L C ((v ◁ own 1 ty)::T') (subst x v e)) →
+    (∀ (v : val), typed_body E L C ((v ◁ own 1 ty)::T') (subst x v e)) →
     typed_body E L C T (letalloc: x := p in e).
   Proof.
     intros. eapply type_let'.
@@ -246,7 +246,8 @@ Section typing.
     Closed [] p → Closed (x :b: []) e →
     typed_read E L ty1 ty ty2 →
     tctx_extract_hasty E L p ty1 T T' →
-    (∀ v, typed_body E L C ((v ◁ own (ty.(ty_size)) ty)::(p ◁ ty2)::T') (subst x v e)) →
+    (∀ (v : val),
+        typed_body E L C ((v ◁ own (ty.(ty_size)) ty)::(p ◁ ty2)::T') (subst x v e)) →
     typed_body E L C T (letalloc: x :={ty.(ty_size)} !p in e).
   Proof.
     intros. eapply type_let'.
diff --git a/theories/typing/product_split.v b/theories/typing/product_split.v
index 11a8f4967fec1292d011a30001f79b89e34a37eb..261a2d369a0303213a973268657cdf7ad9696db1 100644
--- a/theories/typing/product_split.v
+++ b/theories/typing/product_split.v
@@ -13,7 +13,7 @@ Section product_split.
     match tyl with
     | [] => []
     | ty :: tyl =>
-      (p +ₗ #off ◁ ptr ty) :: hasty_ptr_offsets p ptr tyl (off + ty.(ty_size))
+      (p +ₗ #off ◁ ptr ty)%TC :: hasty_ptr_offsets p ptr tyl (off + ty.(ty_size))
     end.
 
   Lemma hasty_ptr_offsets_offset (l : loc) p (off1 off2 : nat) ptr tyl tid :
@@ -292,7 +292,7 @@ Section product_split.
   Proof.
     unfold tctx_extract_hasty=>?. apply (tctx_incl_frame_r _ [_] [_;_]).
     rewrite {1}copy_tctx_incl. apply (tctx_incl_frame_r _ [_] [_]).
-    rewrite tctx_split_shr_prod2 -(contains_tctx_incl _ _ [p' ◁ ty]) //.
+    rewrite tctx_split_shr_prod2 -(contains_tctx_incl _ _ [p' ◁ ty]%TC) //.
     apply contains_skip, contains_nil_l.
   Qed.
 
@@ -318,7 +318,7 @@ Section product_split.
   Proof.
     unfold tctx_extract_hasty=>?. apply (tctx_incl_frame_r _ [_] [_;_]).
     rewrite {1}copy_tctx_incl. apply (tctx_incl_frame_r _ [_] [_]).
-    rewrite tctx_split_shr_prod -(contains_tctx_incl _ _ [p' ◁ ty]) //.
+    rewrite tctx_split_shr_prod -(contains_tctx_incl _ _ [p' ◁ ty]%TC) //.
     apply contains_skip, contains_nil_l.
   Qed.
 
@@ -402,4 +402,8 @@ Hint Resolve tctx_extract_merge_own_prod2 tctx_extract_merge_uniq_prod2
              tctx_extract_merge_uniq_prod tctx_extract_merge_shr_prod
      | 150 : lrust_typing.
 
+Hint Extern 0
+     (tctx_extract_hasty _ _ _ _ (hasty_ptr_offsets _ _ _ _) _) =>
+        cbn[hasty_ptr_offsets].
+
 Hint Unfold extract_tyl : lrust_typing.
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index 98e46c54169f43dd3cdcae7b304632c2aca1b1c7..12110588e7cc5a2d5c0869457d8230754ed043d2 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -63,6 +63,8 @@ Section typing.
         ∃ (l : loc) vl, ⌜length vl = ty.(ty_size) ∧ v = #l⌝ ∗ l ↦∗ vl ∗
           (▷ l ↦∗: ty.(ty_own) tid ={F}=∗
             elctx_interp E qE ∗ llctx_interp L qL ∗ ty2.(ty_own) tid [v]))%I.
+            elctx_interp E qE ∗ llctx_interp L qL ∗ ty2.(ty_own) tid [v]).
+  Global Arguments typed_write _%EL _%LL _%T _%T _%T.
 
   (* Technically speaking, we could remvoe the vl quantifiaction here and use
      mapsto_pred instead (i.e., l ↦∗: ty.(ty_own) tid). However, that would
@@ -76,6 +78,7 @@ Section typing.
         ∃ (l : loc) vl q, ⌜v = #l⌝ ∗ l ↦∗{q} vl ∗ ▷ ty.(ty_own) tid vl ∗
               (l ↦∗{q} vl ={F}=∗ na_own tid F ∗ elctx_interp E qE ∗
                               llctx_interp L qL ∗ ty2.(ty_own) tid [v]))%I.
+  Global Arguments typed_read _%EL _%LL _%T _%T _%T.
 End typing.
 
 Notation typed_instruction_ty E L T1 e ty :=
diff --git a/theories/typing/tests/get_x.v b/theories/typing/tests/get_x.v
new file mode 100644
index 0000000000000000000000000000000000000000..b7e263d2614b440b95f8fe782a403c98cb376086
--- /dev/null
+++ b/theories/typing/tests/get_x.v
@@ -0,0 +1,39 @@
+From lrust.lifetime Require Import definitions.
+From lrust.lang Require Import new_delete.
+From lrust.typing Require Import programs product product_split own uniq_bor
+                    shr_bor int function lft_contexts uninit cont.
+
+Section get_x.
+  Context `{typeG Σ}.
+
+  Definition get_x :=
+    (funrec: <> ["p"] → "ret" :=
+       let: "p'" := !"p" in
+       letalloc: "r" := "p'" +â‚— #0 in
+       delete [ #1; "p"] ;; "ret" ["r":expr])%E.
+
+  Lemma get_x_type :
+    typed_instruction_ty [] [] [] get_x
+        (fn (λ α, [☀α])%EL (λ α, [# own 1 (&uniq{α}Π[int; int])])
+            (λ α, own 1 (&shr{α} int))).
+  Proof.
+    apply type_fn; try apply _. move=> /= α ret args. inv_vec args=>p args.
+    inv_vec args. simpl_subst.
+
+    eapply type_let'.
+    { apply _. }
+    { by eapply (type_deref (&uniq{α} _)), read_own_move. }
+    { solve_typing. }
+    intros p'. simpl_subst.
+
+    eapply (type_letalloc_1 (&shr{α}int)); (try solve_typing)=>r. simpl_subst.
+
+    eapply type_let'.
+    { apply _. }
+    { by eapply (type_delete (uninit 1) 1). }
+    { solve_typing. }
+    move=> /= _.
+
+    eapply type_jump with (args := [r]); solve_typing.
+  Qed.
+End get_x.
diff --git a/theories/typing/type_context.v b/theories/typing/type_context.v
index 3c5450f98c6eff25d407d92c94139d765ce2254a..9344e92e463c3102dd5f3feb4807269f7d8fefbb 100644
--- a/theories/typing/type_context.v
+++ b/theories/typing/type_context.v
@@ -13,10 +13,10 @@ Inductive tctx_elt `{typeG Σ} : Type :=
 | TCtx_hasty (p : path) (ty : type)
 | TCtx_blocked (p : path) (κ : lft) (ty : type).
 
-Definition tctx `{typeG Σ} := list tctx_elt.
+Notation tctx := (list tctx_elt).
 
 Delimit Scope lrust_tctx_scope with TC.
-Bind Scope lrust_tctx_scope with tctx tctx_elt.
+Bind Scope lrust_tctx_scope with tctx_elt.
 
 Infix "◁" := TCtx_hasty (at level 70) : lrust_tctx_scope.
 Notation "p ◁{ κ } ty" := (TCtx_blocked p κ ty)
@@ -124,6 +124,7 @@ Section type_context.
   (** Type context *)
   Definition tctx_interp (tid : thread_id) (T : tctx) : iProp Σ :=
     ([∗ list] x ∈ T, tctx_elt_interp tid x)%I.
+  Global Arguments tctx_interp _ _%TC.
 
   Global Instance tctx_interp_permut tid:
     Proper ((≡ₚ) ==> (⊣⊢)) (tctx_interp tid).
@@ -147,6 +148,7 @@ Section type_context.
   (** Copy typing contexts *)
   Class CopyC (T : tctx) :=
     copyc_persistent tid : PersistentP (tctx_interp tid T).
+  Global Arguments CopyC _%TC.
   Global Existing Instances copyc_persistent.
 
   Global Instance tctx_nil_copy : CopyC [].
@@ -163,6 +165,7 @@ Section type_context.
   (** Send typing contexts *)
   Class SendC (T : tctx) :=
     sendc_change_tid tid1 tid2 : tctx_interp tid1 T -∗ tctx_interp tid2 T.
+  Global Arguments SendC _%TC.
 
   Global Instance tctx_nil_send : SendC [].
   Proof. done. Qed.
@@ -182,6 +185,7 @@ Section type_context.
     ∀ tid q1 q2, lft_ctx -∗ elctx_interp E q1 -∗ llctx_interp L q2 -∗
               tctx_interp tid T1 ={⊤}=∗ elctx_interp E q1 ∗ llctx_interp L q2 ∗
                                      tctx_interp tid T2.
+  Global Arguments tctx_incl _%EL _%LL _%TC _%TC.
   Global Instance : ∀ E L, RewriteRelation (tctx_incl E L).
 
   Global Instance tctx_incl_preorder E L : PreOrder (tctx_incl E L).
@@ -248,6 +252,7 @@ Section type_context.
 
   Definition tctx_extract_hasty E L p ty T T' : Prop :=
     tctx_incl E L T ((p ◁ ty)::T').
+  Global Arguments tctx_extract_hasty _%EL _%LL _%E _%T _%TC _%TC.
   Lemma tctx_extract_hasty_cons E L p ty T T' x :
     tctx_extract_hasty E L p ty T T' →
     tctx_extract_hasty E L p ty (x::T) (x::T').
@@ -268,6 +273,7 @@ Section type_context.
 
   Definition tctx_extract_blocked E L p κ ty T T' : Prop :=
     tctx_incl E L T ((p ◁{κ} ty)::T').
+  Global Arguments tctx_extract_blocked _%EL _%LL _%E _ _%T _%TC _%TC.
   Lemma tctx_extract_blocked_cons E L p κ ty T T' x :
     tctx_extract_blocked E L p κ ty T T' →
     tctx_extract_blocked E L p κ ty (x::T) (x::T').
@@ -281,6 +287,7 @@ Section type_context.
 
   Definition tctx_extract_ctx E L T T1 T2 : Prop :=
     tctx_incl E L T1 (T++T2).
+  Global Arguments tctx_extract_ctx _%EL _%LL _%TC _%TC _%TC.
   Lemma tctx_extract_ctx_nil E L T:
     tctx_extract_ctx E L [] T T.
   Proof. by unfold tctx_extract_ctx. Qed.
@@ -309,6 +316,7 @@ Section type_context.
 
   Class UnblockTctx (κ : lft) (T1 T2 : tctx) : Prop :=
     unblock_tctx : ∀ tid, [†κ] -∗ tctx_interp tid T1 ={⊤}=∗ tctx_interp tid T2.
+  Global Arguments UnblockTctx _ _%TC _%TC.
 
   Global Instance unblock_tctx_nil κ : UnblockTctx κ [] [].
   Proof. by iIntros (tid) "_ $". Qed.
diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v
index 32bc08a56ca8cdbe9e06165c475bf270695261f0..5920a3c2367eea80e508406be9d501bc66cf2eeb 100644
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
@@ -201,6 +201,16 @@ Section typing.
     by apply (tctx_incl_frame_r _ [_] [_]), subtype_tctx_incl, shr_mono'.
   Qed.
 
+  Lemma tctx_extract_hasty_share_samelft E L p ty ty' κ T :
+    lctx_lft_alive E L κ → subtype E L ty' ty →
+    tctx_extract_hasty E L p (&shr{κ}ty) ((p ◁ &uniq{κ}ty')::T)
+                                         ((p ◁ &shr{κ}ty')::T).
+  Proof.
+    intros. apply (tctx_incl_frame_r _ [_] [_;_]).
+    rewrite tctx_share // {1}copy_tctx_incl.
+    by apply (tctx_incl_frame_r _ [_] [_]), subtype_tctx_incl, shr_mono'.
+  Qed.
+
   Lemma tctx_extract_hasty_reborrow E L p ty ty' κ κ' T :
     lctx_lft_incl E L κ' κ → eqtype E L ty ty' →
     tctx_extract_hasty E L p (&uniq{κ'}ty) ((p ◁ &uniq{κ}ty')::T)
@@ -246,3 +256,4 @@ End typing.
 
 Hint Resolve uniq_mono' uniq_proper' tctx_extract_hasty_share
              tctx_extract_hasty_reborrow : lrust_typing.
+Hint Resolve tctx_extract_hasty_share_samelft | 0 : lrust_typing.