show that bor_shorten can be derived

theories/lifetime/lifetime.v

@@ -26,6 +26,14 @@ Section derived.
 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.*)
+Lemma bor_shorten_ κ κ' P : κ ⊑ κ' -∗ &{κ'}P -∗ &{κ}P.
+Proof.
+  iIntros "#Hκκ'". rewrite !bor_unfold_idx. iDestruct 1 as (i) "[#? ?]".
+  iExists i. iFrame. by iApply idx_bor_shorten.
+Qed.
+
 Lemma bor_acc_atomic_cons E κ P :
   ↑lftN ⊆ E →
   lft_ctx -∗ &{κ} P ={E,E∖↑lftN}=∗

theories/lifetime/lifetime_sig.v

@@ -102,6 +102,8 @@ Module Type lifetime_sig.
   Parameter bor_fake : ∀ E κ P,
     ↑lftN ⊆ E → lft_ctx -∗ [†κ] ={E}=∗ &{κ}P.
 
+  (* This is in the signature only to share the derived proof between the
+     model and the outside. *)
   Parameter bor_shorten : ∀ κ κ' P, κ ⊑ κ' -∗ &{κ'}P -∗ &{κ}P.
 
   Parameter bor_sep : ∀ E κ P Q,