diff --git a/theories/typing/borrow.v b/theories/typing/borrow.v
index f96250b8ac2ef87fd90481ea8f71bdf0ffeca38e..64aff4a2ac21274319b28c395151a8f45e7c542e 100644
--- a/theories/typing/borrow.v
+++ b/theories/typing/borrow.v
@@ -28,7 +28,7 @@ Section borrow.
   Lemma tctx_extract_hasty_borrow E L p n ty κ T :
     tctx_extract_hasty E L p (&uniq{κ}ty) ((p ◁ own n ty)::T)
                        ((p ◁{κ} own n ty)::T).
-  Proof. apply (tctx_incl_frame_r E L _ [_] [_;_]), tctx_borrow. Qed.
+  Proof. apply (tctx_incl_frame_r _ [_] [_;_]), tctx_borrow. Qed.
 
   (* See the comment above [tctx_extract_hasty_share] in [uniq_bor.v]. *)
   Lemma tctx_extract_hasty_borrow_share E L p ty ty' κ n T :
@@ -36,11 +36,8 @@ Section borrow.
     tctx_extract_hasty E L p (&shr{κ}ty) ((p ◁ own n ty')::T)
                        ((p ◁ &shr{κ}ty')::(p ◁{κ} own n ty')::T).
   Proof.
-    intros. apply (tctx_incl_frame_r E L _ [_] [_;_;_]). etrans.
-    { by apply tctx_borrow. }
-    apply (tctx_incl_frame_r E L _ [_] [_;_]). etrans.
-    by apply tctx_share. etrans. by apply copy_tctx_incl, _.
-    by apply (tctx_incl_frame_r E L _ [_] [_]), subtype_tctx_incl, shr_mono'.
+    intros. apply (tctx_incl_frame_r _ [_] [_;_;_]). rewrite ->tctx_borrow.
+    apply (tctx_incl_frame_r _ [_] [_;_]). rewrite ->tctx_share; solve_typing.
   Qed.
 
   Lemma type_deref_uniq_own {E L} κ p n ty :
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 59ab07fe31d8cd4cc6c7a65bbc0582c1dc786933..ac9c37cbed279b54c8335cf2de84ca033ce6435b 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -210,7 +210,7 @@ Section typing.
     rewrite -typed_body_mono /flip; last done; first by eapply type_call.
     - etrans. eapply (incl_cctx_incl _ [_]); first by intros ? ->%elem_of_list_singleton.
       apply cctx_incl_cons_match; first done. intros args. inv_vec args=>ret q. inv_vec q. done.
-    - etrans; last by apply (tctx_incl_frame_l _ _ [_]).
+    - etrans; last by apply (tctx_incl_frame_l [_]).
       apply copy_elem_of_tctx_incl; last done. apply _.
   Qed.
 
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index 0ec04a9c1c36df26decc23e56b82e22b17e1483b..fb676f682297418b0ba991a1724befe185136490 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -340,6 +340,7 @@ Section elctx_incl.
     ∀ F, ↑lftN ⊆ F → elctx_interp_0 E -∗ ⌜llctx_interp_0 L⌝ -∗
     ∀ 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.
 
   Global Instance elctx_incl_preorder : PreOrder elctx_incl.
   Proof.
@@ -376,10 +377,9 @@ Section elctx_incl.
     iMod ("Hclose2" with "[$HE2 $HE2']") as "$".
     done.
   Qed.
-
   Global Instance elctx_incl_cons_proper x :
     Proper (elctx_incl ==> elctx_incl) (cons x).
-  Proof. intros ???. by apply (elctx_incl_app_proper [_] [_]). Qed.
+  Proof. by apply (elctx_incl_app_proper [_] [_]). Qed.
 
   Lemma elctx_incl_dup E1 :
     elctx_incl E1 (E1 ++ E1).
@@ -403,7 +403,7 @@ Section elctx_incl.
   Lemma elctx_incl_lft_alive E1 E2 κ :
     lctx_lft_alive E1 [] κ → elctx_incl E1 E2 → elctx_incl E1 ((☀κ) :: E2).
   Proof.
-    intros Hκ HE2. rewrite ->elctx_incl_dup.
+    intros Hκ HE2. rewrite (elctx_incl_dup E1).
     apply (elctx_incl_app_proper _ [_]); last done.
     apply elctx_sat_incl. apply elctx_sat_alive, elctx_sat_nil; first done.
   Qed.
@@ -446,6 +446,6 @@ Lemma elctx_incl_lft_incl_alive `{invG Σ, lftG Σ} E L E1 E2 κ κ' :
   lctx_lft_incl (E ++ E1) L κ κ' → elctx_incl E L E1 E2 →
   elctx_incl E L ((☀κ) :: E1) ((☀κ') :: E2).
 Proof.
-  intros Hκκ' ->%(elctx_incl_lft_incl _ _ _ _ _ _ Hκκ').
+  move=> ? /elctx_incl_lft_incl -> //.
   apply (elctx_incl_app_proper _ _ [_; _] [_]); solve_typing.
 Qed.
diff --git a/theories/typing/product.v b/theories/typing/product.v
index 58063ec67167a994549de0d72c45bab19b54278f..705ae108604ad8cec277027f098453c0701480e0 100644
--- a/theories/typing/product.v
+++ b/theories/typing/product.v
@@ -244,6 +244,6 @@ Section typing.
   Proof. by rewrite -prod_flatten_r -prod_flatten_l. Qed.
 End typing.
 
-
 Hint Resolve product_mono' product_proper' : lrust_typing.
 Hint Resolve product2_mono' product2_proper' | 100 : lrust_typing.
+Hint Opaque product : lrust_typing.
diff --git a/theories/typing/product_split.v b/theories/typing/product_split.v
index 82a97ff6b4e1a11bb355f14c0b94234f37311aa8..928fecfb2af4405841bd8b3cbda8ebac0d8b0fbb 100644
--- a/theories/typing/product_split.v
+++ b/theories/typing/product_split.v
@@ -12,7 +12,8 @@ Section product_split.
   Fixpoint hasty_ptr_offsets (p : path) (ptr: type → type) tyl (off : nat) : tctx :=
     match tyl with
     | [] => []
-    | ty :: tyl => (p +ₗ #off ◁ ptr ty) :: hasty_ptr_offsets p ptr tyl (off + ty.(ty_size))
+    | ty :: tyl =>
+      (p +ₗ #off ◁ ptr ty) :: 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 :
@@ -36,7 +37,8 @@ Section product_split.
     (∀ tid ty vl, (ptr ty).(ty_own) tid vl -∗ ⌜∃ l : loc, vl = [(#l) : val]⌝) →
     ∀ p, tctx_incl E L [p ◁ ptr $ product tyl] (hasty_ptr_offsets p ptr tyl 0).
   Proof.
-    iIntros (Hsplit Hloc p tid q1 q2) "#LFT HE HL H". iInduction tyl as [|ty tyl IH] "IH" forall (p).
+    iIntros (Hsplit Hloc p tid q1 q2) "#LFT HE HL H".
+    iInduction tyl as [|ty tyl IH] "IH" forall (p).
     { iFrame "HE HL". rewrite tctx_interp_nil. done. }
     rewrite product_cons. iMod (Hsplit with "LFT HE HL H") as "(HE & HL & H)".
     cbn -[tctx_elt_interp]. rewrite tctx_interp_cons tctx_interp_singleton tctx_interp_cons.
@@ -46,7 +48,7 @@ Section product_split.
     { iExists #l. iSplit; last done. simpl; by rewrite Hp shift_loc_0. }
     iMod ("IH" with "* HE HL [Htyl]") as "($ & $ & Htyl)".
     { rewrite tctx_interp_singleton //. }
-    iClear "IH". rewrite (hasty_ptr_offsets_offset l) // -plus_n_O //. 
+    iClear "IH". rewrite (hasty_ptr_offsets_offset l) // -plus_n_O //.
   Qed.
 
   Lemma tctx_merge_ptr_prod E L ptr tyl :
@@ -57,14 +59,15 @@ Section product_split.
     (∀ tid ty vl, (ptr ty).(ty_own) tid vl -∗ ⌜∃ l : loc, vl = [(#l) : val]⌝) →
     ∀ p, tctx_incl E L (hasty_ptr_offsets p ptr tyl 0) [p ◁ ptr $ product tyl].
   Proof.
-    iIntros (Hptr Htyl Hmerge Hloc p tid q1 q2) "#LFT HE HL H". iInduction tyl as [|ty tyl IH] "IH" forall (p Htyl); first done.
+    iIntros (Hptr Htyl Hmerge Hloc p tid q1 q2) "#LFT HE HL H".
+    iInduction tyl as [|ty tyl IH] "IH" forall (p Htyl); first done.
     rewrite product_cons. rewrite /= tctx_interp_singleton tctx_interp_cons.
     iDestruct "H" as "[Hty Htyl]". iDestruct "Hty" as (v) "[Hp Hty]". iDestruct "Hp" as %Hp. 
     iDestruct (Hloc with "Hty") as %[l [=->]].
     assert (eval_path p = Some #l) as Hp'.
     { move:Hp. simpl. clear. destruct (eval_path p); last done.
       destruct v; try done. destruct l0; try done. rewrite shift_loc_0. done. }
-    clear Hp. destruct tyl. 
+    clear Hp. destruct tyl.
     { iDestruct (elctx_interp_persist with "HE") as "#HE'".
       iDestruct (llctx_interp_persist with "HL") as "#HL'". iFrame "HE HL". 
       iClear "IH Htyl". simpl. iExists #l. rewrite product_nil. iSplitR; first done.
@@ -74,7 +77,8 @@ Section product_split.
     iMod ("IH" with "* [] HE HL [Htyl]") as "(HE & HL & Htyl)"; first done.
     { change (ty_size ty) with (0+ty_size ty)%nat at 1.
       rewrite plus_comm -hasty_ptr_offsets_offset //. }
-    iClear "IH". iMod (Hmerge with "LFT HE HL [Hty Htyl]") as "($ & $ & ?)"; last by rewrite tctx_interp_singleton.
+    iClear "IH". iMod (Hmerge with "LFT HE HL [Hty Htyl]") as "($ & $ & ?)";
+                   last by rewrite tctx_interp_singleton.
     rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton. iFrame.
     iExists #l. iSplit; done.
   Qed.
@@ -126,8 +130,7 @@ Section product_split.
   Qed.
 
   Lemma tctx_split_own_prod E L n tyl p :
-    tctx_incl E L [p ◁ own n $ product tyl]
-                  (hasty_ptr_offsets p (own n) tyl 0).
+    tctx_incl E L [p ◁ own n $ product tyl] (hasty_ptr_offsets p (own n) tyl 0).
   Proof.
     apply tctx_split_ptr_prod.
     - intros. apply tctx_split_own_prod2.
@@ -146,14 +149,14 @@ Section product_split.
   Qed.
 
   (** Unique borrows *)
-  Lemma tctx_split_uniq_bor_prod2 E L p κ ty1 ty2 :
-    tctx_incl E L [p ◁ uniq_bor κ $ product2 ty1 ty2]
-                  [p ◁ uniq_bor κ ty1; p +ₗ #ty1.(ty_size) ◁ uniq_bor κ ty2].
+  Lemma tctx_split_uniq_prod2 E L p κ ty1 ty2 :
+    tctx_incl E L [p ◁ &uniq{κ} product2 ty1 ty2]
+                  [p ◁ &uniq{κ} ty1; p +ₗ #ty1.(ty_size) ◁ &uniq{κ} ty2].
   Proof.
     iIntros (tid q1 q2) "#LFT $ $ H".
     rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton.
     iDestruct "H" as (v) "[Hp H]". iDestruct "Hp" as %Hp.
-    iDestruct "H" as (l P) "[[EQ #HPiff] HP]". iDestruct "EQ" as %[=->]. 
+    iDestruct "H" as (l P) "[[EQ #HPiff] HP]". iDestruct "EQ" as %[=->].
     iMod (bor_iff with "LFT [] HP") as "Hown". set_solver. by eauto.
     rewrite /= split_prod_mt. iMod (bor_sep with "LFT Hown") as "[H1 H2]".
     set_solver. rewrite /tctx_elt_interp /=.
@@ -161,9 +164,9 @@ Section product_split.
                   iExists _, _; erewrite <-uPred.iff_refl; auto.
   Qed.
 
-  Lemma tctx_merge_uniq_bor_prod2 E L p κ ty1 ty2 :
-    tctx_incl E L [p ◁ uniq_bor κ ty1; p +ₗ #ty1.(ty_size) ◁ uniq_bor κ ty2]
-                  [p ◁ uniq_bor κ $ product2 ty1 ty2].
+  Lemma tctx_merge_uniq_prod2 E L p κ ty1 ty2 :
+    tctx_incl E L [p ◁ &uniq{κ} ty1; p +ₗ #ty1.(ty_size) ◁ &uniq{κ} ty2]
+                  [p ◁ &uniq{κ} product2 ty1 ty2].
   Proof.
     iIntros (tid q1 q2) "#LFT $ $ H".
     rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton.
@@ -179,36 +182,36 @@ Section product_split.
     rewrite split_prod_mt. iApply (bor_combine with "LFT Hown1 Hown2"). set_solver.
   Qed.
 
-  Lemma uniq_bor_is_ptr κ ty tid (vl : list val) :
-    ty_own (uniq_bor κ ty) tid vl -∗ ⌜∃ l : loc, vl = [(#l) : val]⌝.
+  Lemma uniq_is_ptr κ ty tid (vl : list val) :
+    ty_own (&uniq{κ} ty) tid vl -∗ ⌜∃ l : loc, vl = [(#l) : val]⌝.
   Proof.
     iIntros "H". iDestruct "H" as (l P) "[[% _] _]". iExists l. done.
   Qed.
 
-  Lemma tctx_split_uniq_bor_prod E L κ tyl p :
-    tctx_incl E L [p ◁ uniq_bor κ $ product tyl]
+  Lemma tctx_split_uniq_prod E L κ tyl p :
+    tctx_incl E L [p ◁ &uniq{κ} product tyl]
                   (hasty_ptr_offsets p (uniq_bor κ) tyl 0).
   Proof.
     apply tctx_split_ptr_prod.
-    - intros. apply tctx_split_uniq_bor_prod2.
-    - intros. apply uniq_bor_is_ptr.
+    - intros. apply tctx_split_uniq_prod2.
+    - intros. apply uniq_is_ptr.
   Qed.
 
-  Lemma tctx_merge_uniq_bor_prod E L κ tyl :
+  Lemma tctx_merge_uniq_prod E L κ tyl :
     tyl ≠ [] →
     ∀ p, tctx_incl E L (hasty_ptr_offsets p (uniq_bor κ) tyl 0)
-                   [p ◁ uniq_bor κ $ product tyl].
+                   [p ◁ &uniq{κ} product tyl].
   Proof.
     intros. apply tctx_merge_ptr_prod; try done.
     - apply _.
-    - intros. apply tctx_merge_uniq_bor_prod2.
-    - intros. apply uniq_bor_is_ptr.
+    - intros. apply tctx_merge_uniq_prod2.
+    - intros. apply uniq_is_ptr.
   Qed.
 
   (** Shared borrows *)
-  Lemma tctx_split_shr_bor_prod2 E L p κ ty1 ty2 :
-    tctx_incl E L [p ◁ shr_bor κ $ product2 ty1 ty2]
-                  [p ◁ shr_bor κ ty1; p +ₗ #ty1.(ty_size) ◁ shr_bor κ ty2].
+  Lemma tctx_split_shr_prod2 E L p κ ty1 ty2 :
+    tctx_incl E L [p ◁ &shr{κ} product2 ty1 ty2]
+                  [p ◁ &shr{κ} ty1; p +ₗ #ty1.(ty_size) ◁ &shr{κ} ty2].
   Proof.
     iIntros (tid q1 q2) "#LFT $ $ H".
     rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton.
@@ -218,9 +221,9 @@ Section product_split.
       iExists _; iSplitR; done.
   Qed.
 
-  Lemma tctx_merge_shr_bor_prod2 E L p κ ty1 ty2 :
-    tctx_incl E L [p ◁ shr_bor κ ty1; p +ₗ #ty1.(ty_size) ◁ shr_bor κ ty2]
-                  [p ◁ shr_bor κ $ product2 ty1 ty2].
+  Lemma tctx_merge_shr_prod2 E L p κ ty1 ty2 :
+    tctx_incl E L [p ◁ &shr{κ} ty1; p +ₗ #ty1.(ty_size) ◁ &shr{κ} ty2]
+                  [p ◁ &shr{κ} product2 ty1 ty2].
   Proof.
     iIntros (tid q1 q2) "#LFT $ $ H".
     rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton.
@@ -233,30 +236,93 @@ Section product_split.
     by iFrame.
   Qed.
 
-
-  Lemma shr_bor_is_ptr κ ty tid (vl : list val) :
-    ty_own (shr_bor κ ty) tid vl -∗ ⌜∃ l : loc, vl = [(#l) : val]⌝.
+  Lemma shr_is_ptr κ ty tid (vl : list val) :
+    ty_own (&shr{κ} ty) tid vl -∗ ⌜∃ l : loc, vl = [(#l) : val]⌝.
   Proof.
     iIntros "H". iDestruct "H" as (l) "[% _]". iExists l. done.
   Qed.
 
-  Lemma tctx_split_shr_bor_prod E L κ tyl p :
-    tctx_incl E L [p ◁ shr_bor κ $ product tyl]
+  Lemma tctx_split_shr_prod E L κ tyl p :
+    tctx_incl E L [p ◁ &shr{κ} product tyl]
                   (hasty_ptr_offsets p (shr_bor κ) tyl 0).
   Proof.
     apply tctx_split_ptr_prod.
-    - intros. apply tctx_split_shr_bor_prod2.
-    - intros. apply shr_bor_is_ptr.
+    - intros. apply tctx_split_shr_prod2.
+    - intros. apply shr_is_ptr.
   Qed.
 
-  Lemma tctx_merge_shr_bor_prod E L κ tyl :
+  Lemma tctx_merge_shr_prod E L κ tyl :
     tyl ≠ [] →
     ∀ p, tctx_incl E L (hasty_ptr_offsets p (shr_bor κ) tyl 0)
-                   [p ◁ shr_bor κ $ product tyl].
+                   [p ◁ &shr{κ} product tyl].
   Proof.
     intros. apply tctx_merge_ptr_prod; try done.
     - apply _.
-    - intros. apply tctx_merge_shr_bor_prod2.
-    - intros. apply shr_bor_is_ptr.
+    - intros. apply tctx_merge_shr_prod2.
+    - intros. apply shr_is_ptr.
+  Qed.
+
+  (* [tctx_extract] stuff. *)
+
+  (* We do not state the extraction lemmas directly, because we want the
+     automation system to be able to perform e.g., borrowing or splitting after
+     splitting. *)
+  Lemma tctx_extract_split_own_prod2 E L p p' n ty ty1 ty2 T T' :
+    tctx_extract_hasty E L p' ty [p ◁ own n ty1; p +ₗ #ty1.(ty_size) ◁ own n ty2] T' →
+    tctx_extract_hasty E L p' ty ((p ◁ own n $ product2 ty1 ty2) :: T) (T' ++ T) .
+  Proof.
+    unfold tctx_extract_hasty. intros ?. apply (tctx_incl_frame_r T [_] (_::_)).
+    by rewrite tctx_split_own_prod2.
+  Qed.
+
+  Lemma tctx_extract_split_uniq_prod2 E L p p' κ ty ty1 ty2 T T' :
+    tctx_extract_hasty E L p' ty
+            [p ◁ &uniq{κ}ty1; p +ₗ #ty1.(ty_size) ◁ &uniq{κ}ty2] T' →
+    tctx_extract_hasty E L p' ty ((p ◁ &uniq{κ} product2 ty1 ty2) :: T) (T' ++ T) .
+  Proof.
+    unfold tctx_extract_hasty=>?. apply (tctx_incl_frame_r T [_] (_::_)).
+    by rewrite tctx_split_uniq_prod2.
+  Qed.
+
+  Lemma tctx_extract_split_shr_prod2 E L p p' κ ty ty1 ty2 T T' :
+    tctx_extract_hasty E L p' ty
+                  [p ◁ &shr{κ}ty1; p +ₗ #ty1.(ty_size) ◁ &shr{κ}ty2] T' →
+    tctx_extract_hasty E L p' ty ((p ◁ &shr{κ} product2 ty1 ty2) :: T)
+                                 ((p ◁ &shr{κ} product2 ty1 ty2) :: T).
+  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]) //.
+    apply contains_skip, contains_nil_l.
+  Qed.
+
+  Lemma tctx_extract_split_own_prod E L p p' n ty tyl T T' :
+    tctx_extract_hasty E L p' ty (hasty_ptr_offsets p (own n) tyl 0) T' →
+    tctx_extract_hasty E L p' ty ((p ◁ own n $ Π tyl) :: T) (T' ++ T).
+  Proof.
+    unfold tctx_extract_hasty=>?. apply (tctx_incl_frame_r T [_] (_::_)).
+    by rewrite tctx_split_own_prod.
+  Qed.
+
+  Lemma tctx_extract_split_uniq_prod E L p p' κ ty tyl T T' :
+    tctx_extract_hasty E L p' ty (hasty_ptr_offsets p (uniq_bor κ) tyl 0) T' →
+    tctx_extract_hasty E L p' ty ((p ◁ &uniq{κ} Π tyl) :: T) (T' ++ T).
+  Proof.
+    unfold tctx_extract_hasty=>?. apply (tctx_incl_frame_r T [_] (_::_)).
+    by rewrite tctx_split_uniq_prod.
+  Qed.
+
+  Lemma tctx_extract_split_shr_prod E L p p' κ ty tyl T T' :
+    tctx_extract_hasty E L p' ty (hasty_ptr_offsets p (shr_bor κ) tyl 0) T' →
+    tctx_extract_hasty E L p' ty ((p ◁ &shr{κ} Π tyl) :: T) ((p ◁ &shr{κ} Π tyl) :: T).
+  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]) //.
+    apply contains_skip, contains_nil_l.
   Qed.
 End product_split.
+
+Hint Resolve tctx_extract_split_own_prod2 tctx_extract_split_uniq_prod2
+             tctx_extract_split_shr_prod2 tctx_extract_split_own_prod
+             tctx_extract_split_uniq_prod tctx_extract_split_shr_prod : lrust_typing.
diff --git a/theories/typing/type_context.v b/theories/typing/type_context.v
index b9a465578b9bbe695659d0d9bef3ecefea5b7eb2..3c5450f98c6eff25d407d92c94139d765ce2254a 100644
--- a/theories/typing/type_context.v
+++ b/theories/typing/type_context.v
@@ -182,6 +182,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 Instance : ∀ E L, RewriteRelation (tctx_incl E L).
 
   Global Instance tctx_incl_preorder E L : PreOrder (tctx_incl E L).
   Proof.
@@ -205,10 +206,14 @@ Section type_context.
     iMod (Hincl1 with "LFT HE HL H1") as "(HE & HL & $)".
     iApply (Hincl2 with "LFT HE HL H2").
   Qed.
-  Lemma tctx_incl_frame_l E L T T1 T2 :
+  Global Instance tctx_incl_cons E L x :
+    Proper (tctx_incl E L ==> tctx_incl E L) (cons x).
+  Proof. by apply (tctx_incl_app E L [_] [_]). Qed.
+
+  Lemma tctx_incl_frame_l {E L} T T1 T2 :
     tctx_incl E L T1 T2 → tctx_incl E L (T++T1) (T++T2).
   Proof. by apply tctx_incl_app. Qed.
-  Lemma tctx_incl_frame_r E L T T1 T2 :
+  Lemma tctx_incl_frame_r {E L} T T1 T2 :
     tctx_incl E L T1 T2 → tctx_incl E L (T1++T) (T2++T).
   Proof. by intros; apply tctx_incl_app. Qed.
 
@@ -223,8 +228,8 @@ Section type_context.
     (p ◁ ty)%TC ∈ T → tctx_incl E L T ((p ◁ ty) :: T).
   Proof.
     remember (p ◁ ty)%TC. induction 1 as [|???? IH]; subst.
-    - apply (tctx_incl_frame_r E L _ [_] [_;_]), copy_tctx_incl, _.
-    - etrans. by apply (tctx_incl_frame_l E L [_]), IH, reflexivity.
+    - apply (tctx_incl_frame_r _ [_] [_;_]), copy_tctx_incl, _.
+    - etrans. by apply (tctx_incl_frame_l [_]), IH, reflexivity.
       apply contains_tctx_incl, contains_swap.
   Qed.
 
@@ -246,23 +251,19 @@ Section type_context.
   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').
-  Proof.
-    move=> /(tctx_incl_frame_l E L [x]) /= Hincl. rewrite /tctx_extract_hasty.
-    etrans; first done. apply contains_tctx_incl, contains_swap.
-  Qed.
+  Proof. unfold tctx_extract_hasty=>->. apply contains_tctx_incl, contains_swap. Qed.
   Lemma tctx_extract_hasty_here_copy E L p ty ty' T `{!Copy ty} :
     subtype E L ty ty' →
     tctx_extract_hasty E L p ty' ((p ◁ ty)::T) ((p ◁ ty)::T).
   Proof.
-    intros. apply (tctx_incl_frame_r E L _ [_] [_;_]).
+    intros. apply (tctx_incl_frame_r _ [_] [_;_]).
     etrans; first by apply copy_tctx_incl, _.
-    by apply (tctx_incl_frame_r E L _ [_] [_]), subtype_tctx_incl.
+    by apply (tctx_incl_frame_r _ [_] [_]), subtype_tctx_incl.
   Qed.
   Lemma tctx_extract_hasty_here E L p ty ty' T :
     subtype E L ty ty' → tctx_extract_hasty E L p ty' ((p ◁ ty)::T) T.
   Proof.
-    intros. apply (tctx_incl_frame_r E L _ [_] [_]).
-    by apply subtype_tctx_incl.
+    intros. by apply (tctx_incl_frame_r _ [_] [_]), subtype_tctx_incl.
   Qed.
 
   Definition tctx_extract_blocked E L p κ ty T T' : Prop :=
@@ -271,12 +272,12 @@ Section type_context.
     tctx_extract_blocked E L p κ ty T T' →
     tctx_extract_blocked E L p κ ty (x::T) (x::T').
   Proof.
-    move=> /(tctx_incl_frame_l E L [x]) /= Hincl. rewrite /tctx_extract_blocked.
+    move=> /(tctx_incl_frame_l [x]) /= Hincl. rewrite /tctx_extract_blocked.
     etrans; first done. apply contains_tctx_incl, contains_swap.
   Qed.
   Lemma tctx_extract_blocked_here E L p κ ty T :
     tctx_extract_blocked E L p κ ty ((p ◁{κ} ty)::T) T.
-  Proof. intros. by apply (tctx_incl_frame_r E L _ [_] [_]). Qed.
+  Proof. intros. by apply (tctx_incl_frame_r _ [_] [_]). Qed.
 
   Definition tctx_extract_ctx E L T T1 T2 : Prop :=
     tctx_incl E L T1 (T++T2).
@@ -286,24 +287,18 @@ Section type_context.
   Lemma tctx_extract_ctx_hasty E L T T1 T2 T3 p ty:
     tctx_extract_hasty E L p ty T1 T2 → tctx_extract_ctx E L T T2 T3 →
     tctx_extract_ctx E L ((p ◁ ty)::T) T1 T3.
-  Proof.
-    intros. rewrite /tctx_extract_ctx. etrans; first done.
-    by apply (tctx_incl_frame_l _ _ [_]).
-  Qed.
+  Proof. unfold tctx_extract_ctx, tctx_extract_hasty=>->->//. Qed.
   Lemma tctx_extract_ctx_blocked E L T T1 T2 T3 p κ ty:
     tctx_extract_blocked E L p κ ty T1 T2 → tctx_extract_ctx E L T T2 T3 →
     tctx_extract_ctx E L ((p ◁{κ} ty)::T) T1 T3.
-  Proof.
-    intros. rewrite /tctx_extract_ctx. etrans; first done.
-    by apply (tctx_incl_frame_l _ _ [_]).
-  Qed.
+  Proof. unfold tctx_extract_ctx, tctx_extract_blocked=>->->//. Qed.
 
   Lemma tctx_extract_ctx_incl E L T T' T0:
     tctx_extract_ctx E L T' T T0 →
     tctx_incl E L T T'.
   Proof.
-    intros. etrans; first done. rewrite {2}(app_nil_end T').
-    apply tctx_incl_frame_l, contains_tctx_incl, contains_nil_l.
+    unfold tctx_extract_ctx=>->.
+      by apply contains_tctx_incl, contains_inserts_r.
   Qed.
 
   (* Unblocking a type context. *)
diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v
index 6795ade5c22652a29f31c58009627e8e9b708db0..bc8db8522fcaf7d706d839aa9097d3f860d97fe9 100644
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
@@ -195,11 +195,10 @@ Section typing.
     tctx_extract_hasty E L p (&shr{κ}ty) ((p ◁ &uniq{κ'}ty')::T)
                        ((p ◁ &shr{κ}ty')::(p ◁{κ} &uniq{κ'}ty')::T).
   Proof.
-    intros. apply (tctx_incl_frame_r E L _ [_] [_;_;_]). etrans.
-    { by apply tctx_reborrow_uniq. }
-    apply (tctx_incl_frame_r E L _ [_] [_;_]). etrans.
-    by apply tctx_share. etrans. by apply copy_tctx_incl, _.
-    by apply (tctx_incl_frame_r E L _ [_] [_]), subtype_tctx_incl, shr_mono'.
+    intros. apply (tctx_incl_frame_r _ [_] [_;_;_]).
+    rewrite tctx_reborrow_uniq //. 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 :
@@ -207,9 +206,8 @@ Section typing.
     tctx_extract_hasty E L p (&uniq{κ'}ty) ((p ◁ &uniq{κ}ty')::T)
                        ((p ◁{κ'} &uniq{κ}ty')::T).
   Proof.
-    intros. apply (tctx_incl_frame_r E L _ [_] [_;_]). etrans.
-    by apply tctx_reborrow_uniq.
-    by apply (tctx_incl_frame_r E L _ [_] [_]), subtype_tctx_incl, uniq_mono'.
+    intros. apply (tctx_incl_frame_r _ [_] [_;_]). rewrite tctx_reborrow_uniq //.
+    by apply (tctx_incl_frame_r _ [_] [_]), subtype_tctx_incl, uniq_mono'.
   Qed.
 
   Lemma read_uniq E L κ ty :