diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index a1665a3f95743b5603634f9e61adfe57592c9bd1..a31e1bb06730450d88d3c39d70cc3e14ee59f0a1 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -143,7 +143,8 @@ Section lft_contexts.
 
   Lemma incl_local κ κ' κs : (κ, κs) ∈ L → κ' ∈ κs → incl κ κ'.
   Proof.
-    iIntros (? Hκ'κs) "_ H". iDestruct "H" as %(κ0 & EQ). done. simpl in EQ; subst.
+    iIntros (? Hκ'κs) "_ H". iDestruct "H" as %HL.
+    edestruct HL as [κ0 EQ]. done. simpl in EQ; subst.
     iApply lft_le_incl. etrans; last by apply gmultiset_union_subseteq_l.
     clear -Hκ'κs. induction Hκ'κs.
     - apply gmultiset_union_subseteq_l.