diff --git a/theories/lifetime/lifetime.v b/theories/lifetime/lifetime.v
index 183cdd37a6c5b2430a2e9086c3d8c6f52daacc4c..13271eb54c3193b86f2d28b1c0572cbebc20f836 100644
--- a/theories/lifetime/lifetime.v
+++ b/theories/lifetime/lifetime.v
@@ -27,7 +27,7 @@ Context `{!invG Σ, !lftG Σ}.
 Implicit Types κ : lft.
 
 (* Deriving this just to prove that it can be derived.
-(It is in the signature only for code sharing reasons.*)
+(It is in the signature only for code sharing reasons.) *)
 Lemma bor_shorten_ κ κ' P : κ ⊑ κ' -∗ &{κ'}P -∗ &{κ}P.
 Proof.
   iIntros "#Hκκ'". rewrite !bor_unfold_idx. iDestruct 1 as (i) "[#? ?]".
diff --git a/theories/lifetime/lifetime_sig.v b/theories/lifetime/lifetime_sig.v
index b7b0abf7bb393148272b98515c0c195cf6a5b311..2e275346b04efca7ca73ddaa2a379b01d9957c29 100644
--- a/theories/lifetime/lifetime_sig.v
+++ b/theories/lifetime/lifetime_sig.v
@@ -126,6 +126,8 @@ Module Type lifetime_sig.
     lft_ctx -∗ &{κ,i}P -∗ idx_bor_own q i ={E,E∖↑lftN}=∗
       (▷ P ∗ (▷ P ={E∖↑lftN,E}=∗ idx_bor_own q i)) ∨
                 ([†κ] ∗ |={E∖↑lftN,E}=> idx_bor_own q i).
+  (* We have to expose κ' here as without [lftN] in the mask of the Q-to-P view
+     shift, we cannot turn [†κ'] into [†κ]. *)
   Parameter bor_acc_strong : ∀ E q κ P, ↑lftN ⊆ E →
     lft_ctx -∗ &{κ} P -∗ q.[κ] ={E}=∗ ∃ κ', κ ⊑ κ' ∗ ▷ P ∗
       ∀ Q, ▷ (▷ Q -∗ [†κ'] ={↑lft_userN}=∗ ▷ P) -∗ ▷ Q ={E}=∗ &{κ'} Q ∗ q.[κ].