diff --git a/theories/lifetime/definitions.v b/theories/lifetime/definitions.v
index d98f4dd120fc4f9cfb45fc821bd135a61df8047a..01d78a702fd19d44b541124c8c95f030dff9d9c3 100644
--- a/theories/lifetime/definitions.v
+++ b/theories/lifetime/definitions.v
@@ -200,9 +200,10 @@ Notation "&{ κ , i } P" := (idx_bor κ i P)
 
 Infix "⊑" := lft_incl (at level 70) : uPred_scope.
 
-Typeclasses Opaque lft_tok lft_dead bor_cnt lft_bor_alive lft_bor_dead
+Typeclasses Opaque lft_inv_alive lft_vs_inv lft_vs lft_incl.
+(*Typeclasses Opaque lft_tok lft_dead bor_cnt lft_bor_alive lft_bor_dead
   lft_inh lft_inv_alive lft_vs_inv lft_vs lft_inv_dead lft_inv lft_incl
-  idx_bor_own idx_bor raw_bor bor.
+  idx_bor_own idx_bor raw_bor bor.*)
 
 Section basic_properties.
 Context `{invG Σ, lftG Σ}.
diff --git a/theories/lifetime/primitive.v b/theories/lifetime/primitive.v
index 235510a1decffa187497b69c678922a794ac62c8..8bcdcbd2854683e1e4ee87e03068a8a46a993044 100644
--- a/theories/lifetime/primitive.v
+++ b/theories/lifetime/primitive.v
@@ -393,7 +393,9 @@ Lemma lft_inh_extend E κ P Q :
      (∀ Q', ▷ lft_inh κ true Q' ={E}=∗ ∃ Q'',
             ▷ ▷ (Q' ≡ (P ∗ Q'')) ∗ ▷ P ∗ ▷ lft_inh κ true Q'').
 Proof.
-  rewrite {1}/lft_inh. iDestruct 1 as (PE) "[>HE Hbox]".
+  iIntros (?) "H".
+  Set Typeclasses Debug.
+  unfold lft_inh. iDestruct "H" as (PE) "[>HE Hbox]".
   iMod (slice_insert_empty _ _ true _ P with "Hbox")
     as (γE) "(% & #Hslice & Hbox)".
   iMod (own_inh_update with "HE") as "[HE HE◯]".