diff --git a/theories/lifetime.v b/theories/lifetime.v
index 2956516d7d3a1ae5814d342cd616f12e39e1e6ee..bfa9e8d9e4433c98ae8878bf5c70855980009aa6 100644
--- a/theories/lifetime.v
+++ b/theories/lifetime.v
@@ -47,15 +47,15 @@ Section defs.
   Definition idx_borrow_own (q : Qp) (i : borrow_idx) :=
     own borrow_tok_name (â—¯ {[ i := q ]}).
 
-End defs.
+  Parameter idx_borrow:
+    ∀ `{lifetimeG Σ} (κ : lifetime) (i : borrow_idx) (P : iProp Σ), iProp Σ.
 
-Typeclasses Opaque lft_own lft_dead .
+  Definition borrow (κ : lifetime) (P : iProp Σ) : iProp Σ :=
+    (∃ i, idx_borrow κ i P ∗ idx_borrow_own 1 i)%I.
 
-Parameter idx_borrow:
-  ∀ `{lifetimeG Σ} (κ : lifetime) (i : borrow_idx) (P : iProp Σ), iProp Σ.
+End defs.
 
-Definition borrow `{lifetimeG Σ} (κ : lifetime) (P : iProp Σ) : iProp Σ :=
-  (∃ i, idx_borrow κ i P ∗ idx_borrow_own 1 i)%I.
+Typeclasses Opaque lft_own lft_dead borrow.
 
 (*** Notations  *)