Lennard Gäher
--- a/lifetime/lifetime_sig.v
+++ b/lifetime/lifetime_sig.v
    lft_ctx ={E}=∗
    ∃ p : positive, let κ := positive_to_lft p in ⌜P p⌝ ∗
         (1).[κ] ∗ □ ((1).[κ] ={↑lftN ∪ userE}[userE]▷=∗ [†κ]).
+  Parameter lft_fresh_strong : ∀ κ κ', ∃ i : positive, ∀ m : positive, (i < m)%positive → (positive_to_lft m) ⊓ κ' ≠ κ.
--- a/lifetime/lifetime_sig.v
+++ b/lifetime/lifetime_sig.v
    lft_ctx ={E}=∗
    ∃ p : positive, let κ := positive_to_lft p in ⌜P p⌝ ∗
         (1).[κ] ∗ □ ((1).[κ] ={↑lftN ∪ userE}[userE]▷=∗ [†κ]).
-  Parameter lft_fresh_strong : ∀ κ κ', ∃ i : positive, ∀ m : positive, (i < m)%positive → (positive_to_lft m) ⊓ κ' ≠ κ.
+  (** Given two lifetimes [κ] and [κ'], find a lower bound on atomic lifetimes [m]
+     such that [m ⊓ κ'] is syntactically different from [κ].
+     This is useful in conjunction with [lft_create_strong] to generate
+     fresh lifetimes when using lifetimes as keys to index into a map. *)
+  Parameter lft_fresh_strong : ∀ κ κ', ∃ i : positive,
+    ∀ m : positive, (i < m)%positive → (positive_to_lft m) ⊓ κ' ≠ κ.