adjust name + use new stdpp lemma

lifetime/lifetime_sig.v

@@ -122,7 +122,7 @@ Module Type lifetime_sig.
      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,
+  Parameter lft_fresh : ∀ κ κ', ∃ i : positive,
     ∀ m : positive, (i < m)%positive → (positive_to_lft m) ⊓ κ' ≠ κ.
 
   Parameter bor_create : ∀ E κ P,

lifetime/model/creation.v

@@ -185,21 +185,11 @@ Proof.
     + iRight. iFrame. iPureIntro. by apply lft_dead_in_insert_false.
 Qed.
 
-(* TODO: remove once stdpp!562 is merged *)
-Lemma lower_bound_exists `{FinSet A C} R `{!Transitive R,
-    ∀ x y, Decision (R x y)} `{!Inhabited A} (X : C) :
-  ∃ x, minimal R x X.
-Proof.
-  destruct (set_choose_or_empty X) as [ (y & Ha) | Hne].
-  - edestruct (minimal_exists R X) as (x & Hel & Hmin); first set_solver.
-    exists x. done.
-  - exists inhabitant. intros y Hel. set_solver.
-Qed.
-Lemma lft_fresh_strong κ κ' :
+Lemma lft_fresh κ κ' :
   ∃ i : positive, ∀ m : positive, (i < m)%positive → (positive_to_lft m) ⊓ κ' ≠ κ.
 Proof.
   unfold meet, lft_intersect.
-  destruct (lower_bound_exists (flip Pos.le) (dom κ)) as (i & Ha).
+  destruct (minimal_exists (flip Pos.le) (dom κ)) as (i & Ha).
   exists (i + 1)%positive.
   intros k Hik Heq. subst κ.
   ospecialize (Ha k _ _); simpl in *; [ | lia..].