diff --git a/theories/typing/function.v b/theories/typing/function.v
index c649ca8412eb6f0c485aca05a561f52fee8540c0..59ab07fe31d8cd4cc6c7a65bbc0582c1dc786933 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -209,7 +209,7 @@ Section typing.
     intros Hfn HE HTT' HC HT'T''.
     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; first done. intros args. inv_vec args=>ret q. inv_vec q. done.
+      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 _ _ [_]).
       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 486b54bf78cdafd4c1f570023456b24c6bab8f1c..0ec04a9c1c36df26decc23e56b82e22b17e1483b 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -436,9 +436,9 @@ Hint Resolve
 (* 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.
+  eapply @elem_of_list_here : lrust_typing.
 Hint Extern 1 (@elem_of _ _ (@elem_of_list _) _ (_ :: _)) =>
-  eapply @elem_of_list_further.
+  eapply @elem_of_list_further : lrust_typing.
 
 Hint Resolve lctx_lft_alive_external' | 100 : lrust_typing.