diff --git a/theories/typing/borrow.v b/theories/typing/borrow.v
index d6204fdb569cb9c43db1c712ef5e1ba8bbef5a32..76a658d4d8dbbfa047dbf592ab6330f1ad3171c0 100644
--- a/theories/typing/borrow.v
+++ b/theories/typing/borrow.v
@@ -30,8 +30,7 @@ Section borrow.
     tctx_extract_hasty E L p (&uniq{κ}ty) ((p ◁ own n ty')::T)
                        ((p ◁{κ} own n ty)::T).
   Proof.
-    rewrite tctx_extract_hasty_unfold=>Htyty'.
-    apply (tctx_incl_frame_r _ [_] [_;_]). rewrite subtype_tctx_incl.
+    intros. apply (tctx_incl_frame_r _ [_] [_;_]). rewrite subtype_tctx_incl.
     by apply tctx_borrow. by f_equiv.
   Qed.
 
@@ -41,8 +40,7 @@ Section borrow.
     tctx_extract_hasty E L p (&shr{κ}ty) ((p ◁ own n ty')::T)
                        ((p ◁ &shr{κ}ty')::(p ◁{κ} own n ty')::T).
   Proof.
-    rewrite tctx_extract_hasty_unfold=>??.
-    apply (tctx_incl_frame_r _ [_] [_;_;_]). rewrite ->tctx_borrow.
+    intros. apply (tctx_incl_frame_r _ [_] [_;_;_]). rewrite ->tctx_borrow.
     apply (tctx_incl_frame_r _ [_] [_;_]). rewrite ->tctx_share; solve_typing.
   Qed.
 
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 4890d0cf8a681f173d352cfc4af8d2b743e069a6..6e62148f49683fd65032c9784fac76377b5fe293 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -209,8 +209,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. by inv_vec args.
-    - rewrite tctx_extract_ctx_unfold in HTT'.
-      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/product.v b/theories/typing/product.v
index 9cfb6a6586502d9bfca2d05a2f1b635bb9dbad02..f28f1f02df32d232376e2a52a7737bac8a4eff18 100644
--- a/theories/typing/product.v
+++ b/theories/typing/product.v
@@ -91,17 +91,9 @@ Section product.
       + by iApply "Hs1".
       + rewrite -(_ : ty_size ty11 = ty_size ty12) //. by iApply "Hs2".
   Qed.
-  Lemma product2_mono' E L ty11 ty12 ty21 ty22 :
-    subtype E L ty11 ty12 → subtype E L ty21 ty22 →
-    subtype E L (product2 ty11 ty21) (product2 ty12 ty22).
-  Proof. by intros; apply product2_mono. Qed.
   Global Instance product2_proper E L:
     Proper (eqtype E L ==> eqtype E L ==> eqtype E L) product2.
   Proof. by intros ??[]??[]; split; apply product2_mono. Qed.
-  Lemma product2_proper' E L ty11 ty12 ty21 ty22 :
-    eqtype E L ty11 ty12 → eqtype E L ty21 ty22 →
-    eqtype E L (product2 ty11 ty21) (product2 ty12 ty22).
-  Proof. by intros; apply product2_proper. Qed.
 
   Global Instance product2_copy `{!Copy ty1} `{!Copy ty2} :
     Copy (product2 ty1 ty2).
@@ -243,5 +235,4 @@ Section typing.
 End typing.
 
 Hint Resolve product_mono' product_proper' : lrust_typing.
-Hint Resolve product2_mono' product2_proper' | 100 : lrust_typing.
-Hint Opaque product : lrust_typing.
+Hint Opaque product : lrust_typing typeclass_instances.
diff --git a/theories/typing/product_split.v b/theories/typing/product_split.v
index d2eabaf71b92f17be149dcb2c65d6dcf7d5db809..3029708fa7e04eb565cc30606244af0dba7fbf41 100644
--- a/theories/typing/product_split.v
+++ b/theories/typing/product_split.v
@@ -265,56 +265,25 @@ Section product_split.
   (* 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.
-    rewrite !tctx_extract_hasty_unfold. 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.
-    rewrite !tctx_extract_hasty_unfold=>?. 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.
-    rewrite !tctx_extract_hasty_unfold=>?. 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]%TC) //.
-    apply submseteq_skip, submseteq_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.
-    rewrite !tctx_extract_hasty_unfold=>?. apply (tctx_incl_frame_r T [_] (_::_)).
-    by rewrite tctx_split_own_prod.
+    intros. 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.
-    rewrite !tctx_extract_hasty_unfold=>?. apply (tctx_incl_frame_r T [_] (_::_)).
-    by rewrite tctx_split_uniq_prod.
+    intros. 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.
-    rewrite !tctx_extract_hasty_unfold=>?. apply (tctx_incl_frame_r _ [_] [_;_]).
+    intros. 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]%TC) //.
     apply submseteq_skip, submseteq_nil_l.
@@ -322,33 +291,6 @@ Section product_split.
 
   (* Merging with [tctx_extract]. *)
 
-  Lemma tctx_extract_merge_own_prod2 E L p n ty1 ty2 T1 T2 T3 :
-    tctx_extract_hasty E L p (own n ty1) T1 T2 →
-    tctx_extract_hasty E L (p +ₗ #ty1.(ty_size)) (own n ty2) T2 T3 →
-    tctx_extract_hasty E L p (own n (product2 ty1 ty2)) T1 T3.
-  Proof.
-    rewrite !tctx_extract_hasty_unfold=>->->.
-    apply (tctx_incl_frame_r _ [_;_] [_]), tctx_merge_own_prod2.
-  Qed.
-
-  Lemma tctx_extract_merge_uniq_prod2 E L p κ ty1 ty2 T1 T2 T3 :
-    tctx_extract_hasty E L p (&uniq{κ}ty1) T1 T2 →
-    tctx_extract_hasty E L (p +ₗ #ty1.(ty_size)) (&uniq{κ}ty2) T2 T3 →
-    tctx_extract_hasty E L p (&uniq{κ}product2 ty1 ty2) T1 T3.
-  Proof.
-    rewrite !tctx_extract_hasty_unfold=>->->.
-    apply (tctx_incl_frame_r _ [_;_] [_]), tctx_merge_uniq_prod2.
-  Qed.
-
-  Lemma tctx_extract_merge_shr_prod2 E L p κ ty1 ty2 T1 T2 T3 :
-    tctx_extract_hasty E L p (&shr{κ}ty1) T1 T2 →
-    tctx_extract_hasty E L (p +ₗ #ty1.(ty_size)) (&shr{κ}ty2) T2 T3 →
-    tctx_extract_hasty E L p (&shr{κ}product2 ty1 ty2) T1 T3.
-  Proof.
-    rewrite !tctx_extract_hasty_unfold=>->->.
-    apply (tctx_incl_frame_r _ [_;_] [_]), tctx_merge_shr_prod2.
-  Qed.
-
   Fixpoint extract_tyl E L p (ptr: type → type) tyl (off : nat) T T' : Prop :=
     match tyl with
     | [] => T = T'
@@ -362,8 +304,8 @@ Section product_split.
     extract_tyl E L p ptr tyl 0 T T' →
     tctx_extract_hasty E L p (ptr (Π tyl)) T T'.
   Proof.
-    rewrite /extract_tyl !tctx_extract_hasty_unfold=>Hi Htyl.
-    etrans. 2:by eapply (tctx_incl_frame_r T' _ [_]). revert T Htyl. clear.
+    rewrite /extract_tyl /tctx_extract_hasty=>Hi Htyl.
+    etrans; last by eapply (tctx_incl_frame_r T' _ [_]). revert T Htyl. clear.
     generalize 0%nat. induction tyl=>[T n /= -> //|T n /= [T'' [-> Htyl]]]. f_equiv. auto.
   Qed.
 
@@ -388,13 +330,11 @@ End product_split.
 
 (* We do not want unification to try to unify the definition of these
    types with anything in order to try splitting or merging. *)
-Hint Opaque own uniq_bor shr_bor product product2 tctx_extract_hasty : lrust_typing lrust_typing_merge.
+Hint Opaque own uniq_bor shr_bor product tctx_extract_hasty : lrust_typing lrust_typing_merge.
 
 (* We make sure that splitting is tried before borrowing, so that not
    the entire product is borrowed when only a part is needed. *)
-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
+Hint Resolve tctx_extract_split_own_prod tctx_extract_split_uniq_prod tctx_extract_split_shr_prod
     | 5 : lrust_typing.
 
 (* Merging is also tried after everything, except
@@ -407,8 +347,6 @@ Hint Resolve tctx_extract_split_own_prod2 tctx_extract_split_uniq_prod2
    solve_typing get slow because of that. See:
      https://coq.inria.fr/bugs/show_bug.cgi?id=5304
 *)
-Hint Resolve tctx_extract_merge_own_prod2 tctx_extract_merge_uniq_prod2
-             tctx_extract_merge_shr_prod2 tctx_extract_merge_own_prod
-             tctx_extract_merge_uniq_prod tctx_extract_merge_shr_prod
+Hint Resolve tctx_extract_merge_own_prod tctx_extract_merge_uniq_prod tctx_extract_merge_shr_prod
     | 40 : lrust_typing_merge.
-Hint Unfold extract_tyl.
\ No newline at end of file
+Hint Unfold extract_tyl : lrust_typing.
\ No newline at end of file
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index 8b0844c9ddda6298bff8d72cc751d763f7e701a0..291993faa945f1e6f6ab3a273e89cfdf7ca4f836 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -122,7 +122,7 @@ Section typing_rules.
     tctx_extract_ctx E L T1 T T' →
     (∀ v : val, typed_body E L C (T2 v ++ T') (subst' xb v e')) →
     typed_body E L C T (let: xb := e in e').
-  Proof. rewrite tctx_extract_ctx_unfold. intros ?? -> ?. by eapply type_let'. Qed.
+  Proof. unfold tctx_extract_ctx. intros ?? -> ?. by eapply type_let'. Qed.
 
   Lemma type_seq E L T T' T1 T2 C e e' :
     Closed [] e' →
diff --git a/theories/typing/type_context.v b/theories/typing/type_context.v
index 6989b31e27137a248385d103a3e54a269c899e57..1d1535f1973b77f0affb09743fa6c68be0d91a29 100644
--- a/theories/typing/type_context.v
+++ b/theories/typing/type_context.v
@@ -253,8 +253,6 @@ 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.
-  Definition tctx_extract_hasty_unfold :
-    tctx_extract_hasty = λ E L p ty T T', tctx_incl E L T ((p ◁ ty)::T') := eq_refl.
   Lemma tctx_extract_hasty_further 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').
@@ -292,8 +290,6 @@ Section type_context.
 
   Definition tctx_extract_ctx E L T T1 T2 : Prop :=
     tctx_incl E L T1 (T++T2).
-  Definition tctx_extract_ctx_unfold :
-    tctx_extract_ctx = λ E L T T1 T2, tctx_incl E L T1 (T++T2) := eq_refl.
   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.
diff --git a/theories/typing/type_sum.v b/theories/typing/type_sum.v
index 176924bfbaca817375e335f9fc6e5deaaa2b15b8..037176e2d36a03c3e99fa27fdef7aa448002f833 100644
--- a/theories/typing/type_sum.v
+++ b/theories/typing/type_sum.v
@@ -56,7 +56,7 @@ Section case.
             own n (uninit (list_max (map ty_size tyl) - ty_size ty))) :: T') e ∨
       typed_body E L C ((p ◁ own n (sum tyl)) :: T') e) tyl el →
     typed_body E L C T (case: !p of el).
-  Proof. rewrite tctx_extract_hasty_unfold=>->. apply type_case_own'. Qed.
+  Proof. unfold tctx_extract_hasty=>->. apply type_case_own'. Qed.
 
   Lemma type_case_uniq' E L C T p κ tyl el :
     lctx_lft_alive E L κ →
@@ -113,7 +113,7 @@ Section case.
       typed_body E L C ((p +ₗ #1 ◁ &uniq{κ}ty) :: T') e ∨
       typed_body E L C ((p ◁ &uniq{κ}sum tyl) :: T') e) tyl el →
     typed_body E L C T (case: !p of el).
-  Proof. rewrite tctx_extract_hasty_unfold=>->. apply type_case_uniq'. Qed.
+  Proof. unfold tctx_extract_hasty=>->. apply type_case_uniq'. Qed.
 
   Lemma type_case_shr' E L C T p κ tyl el:
     lctx_lft_alive E L κ →
diff --git a/theories/typing/uninit.v b/theories/typing/uninit.v
index fdf54fe406a566172b76a2fc1e265370d8080ae7..55e8524a2bc87b6243c2c85c12ce958d308d7d35 100644
--- a/theories/typing/uninit.v
+++ b/theories/typing/uninit.v
@@ -85,10 +85,10 @@ Section uninit.
     iSplit.
     - rewrite ty_size_eq. auto.
     - iInduction vl as [|v vl] "IH" forall (n).
-      + iIntros "%". destruct n; done.
+      + iIntros "%". by destruct n; simpl.
       + iIntros (Heq). destruct n; first done. simpl.
         iExists [v], vl. iSplit; first done. iSplit; first done.
-        iApply "IH". by inversion Heq.
+        unfold uninit0, product. iApply "IH". by inversion Heq.
   Qed.
 End uninit.
 
diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v
index f172818914a99c61871a8f9183edd56f8be7f87b..b7393c44ca1432fac5fcc57c2eed98f5f3de1f8a 100644
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
@@ -194,7 +194,7 @@ Section typing.
     tctx_extract_hasty E L p (&shr{κ}ty) ((p ◁ &uniq{κ'}ty')::T)
                        ((p ◁ &shr{κ}ty')::(p ◁{κ} &uniq{κ'}ty')::T).
   Proof.
-    rewrite tctx_extract_hasty_unfold=>???. apply (tctx_incl_frame_r _ [_] [_;_;_]).
+    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'.
@@ -205,7 +205,7 @@ Section typing.
     tctx_extract_hasty E L p (&shr{κ}ty) ((p ◁ &uniq{κ}ty')::T)
                                          ((p ◁ &shr{κ}ty')::T).
   Proof.
-    rewrite tctx_extract_hasty_unfold=>??. apply (tctx_incl_frame_r _ [_] [_;_]).
+    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.
@@ -215,8 +215,7 @@ Section typing.
     tctx_extract_hasty E L p (&uniq{κ'}ty) ((p ◁ &uniq{κ}ty')::T)
                        ((p ◁{κ'} &uniq{κ}ty')::T).
   Proof.
-    rewrite tctx_extract_hasty_unfold=>??.
-    apply (tctx_incl_frame_r _ [_] [_;_]). rewrite tctx_reborrow_uniq //.
+    intros. apply (tctx_incl_frame_r _ [_] [_;_]). rewrite tctx_reborrow_uniq //.
     by apply (tctx_incl_frame_r _ [_] [_]), subtype_tctx_incl, uniq_mono'.
   Qed.