diff --git a/theories/typing/cont_context.v b/theories/typing/cont_context.v
index b403d833f007c89b0da6717a547cffe38486af00..b77593cc052695d267eefc78d0d3c77075767d12 100644
--- a/theories/typing/cont_context.v
+++ b/theories/typing/cont_context.v
@@ -92,7 +92,7 @@ Section cont_context.
     iApply ("H" with "HE * [%]"). by apply HC1C2.
   Qed.
 
-  Lemma cctx_incl_cons E k L n (T1 T2 : vec val n → tctx) C1 C2 :
+  Lemma cctx_incl_cons_match E k L n (T1 T2 : vec val n → tctx) C1 C2 :
     cctx_incl E C1 C2 → (∀ args, tctx_incl E L (T2 args) (T1 args)) →
     cctx_incl E (k ◁cont(L, T1) :: C1) (k ◁cont(L, T2) :: C2).
   Proof.
@@ -111,4 +111,18 @@ Section cont_context.
   Lemma cctx_incl_nil E C : cctx_incl E C [].
   Proof. apply incl_cctx_incl. by set_unfold. Qed.
 
+  Lemma cctx_incl_cons E k L n (T1 T2 : vec val n → tctx) C1 C2 :
+    (k ◁cont(L, T1))%CC ∈ C1 →
+    (∀ args, tctx_incl E L (T2 args) (T1 args)) →
+    cctx_incl E C1 C2 →
+    cctx_incl E C1 (k ◁cont(L, T2) :: C2).
+  Proof.
+    intros Hin ??. rewrite <-cctx_incl_cons_match; try done.
+    iIntros (??) "_ HC HE". iSpecialize ("HC" with "HE").
+    rewrite cctx_interp_cons. iSplit; last done. clear -Hin.
+    iInduction Hin as [] "IH"; rewrite cctx_interp_cons;
+      [iDestruct "HC" as "[$ _]" | iApply "IH"; iDestruct "HC" as "[_ $]"].
+  Qed.
 End cont_context.
+
+Hint Resolve cctx_incl_nil cctx_incl_cons : lrust_typing.
diff --git a/theories/typing/function.v b/theories/typing/function.v
index fdcb02f47938ece3ad6e6ea38829d69d7dfda45b..c649ca8412eb6f0c485aca05a561f52fee8540c0 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -268,4 +268,3 @@ Section typing.
 End typing.
 
 Hint Resolve fn_subtype_full : lrust_typing.
-Hint Constructors Forall2 elem_of_list: lrust_typing.
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index a6a662669f5a0c98cf2d686daef6ead696f17656..486b54bf78cdafd4c1f570023456b24c6bab8f1c 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -424,7 +424,7 @@ End elctx_incl.
 
 Ltac solve_typing := by eauto 100 with lrust_typing.
 
-Hint Constructors Forall : lrust_typing.
+Hint Constructors Forall Forall2 : lrust_typing.
 Hint Resolve
      lctx_lft_incl_relf lctx_lft_incl_static lctx_lft_incl_local'
      lctx_lft_incl_external'
diff --git a/theories/typing/product.v b/theories/typing/product.v
index dbb855fff2398cf05eab6076e2405299a60c0190..58063ec67167a994549de0d72c45bab19b54278f 100644
--- a/theories/typing/product.v
+++ b/theories/typing/product.v
@@ -246,5 +246,4 @@ End typing.
 
 
 Hint Resolve product_mono' product_proper' : lrust_typing.
-Hint Constructors Forall2 : lrust_typing.
 Hint Resolve product2_mono' product2_proper' | 100 : lrust_typing.
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index 79bee07aeb709f42720aa076b1ce5df6b7a659e3..6cb8c72a6ea9dfa3ccd4b8c0b1ca5a05e40d2de8 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -238,4 +238,3 @@ Notation "Σ[ ty1 ; .. ; tyn ]" :=
   (sum (cons ty1 (..(cons tyn nil)..))) : lrust_typing.
 
 Hint Resolve sum_mono' sum_proper' : lrust_typing.
-Hint Constructors Forall2 : lrust_typing.