From db2b13d2cc701cb3c93aafcab1d45915fd055922 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 16 Aug 2024 09:44:49 +0200
Subject: [PATCH] Forward compatibility fix for
 https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/555

---
 lifetime/model/primitive.v | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/lifetime/model/primitive.v b/lifetime/model/primitive.v
index 3405d59a..c3c4f2ac 100644
--- a/lifetime/model/primitive.v
+++ b/lifetime/model/primitive.v
@@ -38,7 +38,8 @@ Lemma own_ilft_auth_agree (I : gmap lft lft_names) κ γs :
 Proof.
   iIntros "HI Hκ". iDestruct (own_valid_2 with "HI Hκ")
     as %[[? [Hl ?]]%singleton_included_l _]%auth_both_valid_discrete.
-  unfold to_ilftUR in *. simplify_map_eq.
+  revert Hl. rewrite /to_ilftUR lookup_fmap.
+  case: (I !! _)=> [γs'|] Hl; first by eauto.
   destruct (fmap_Some_equiv_1 _ _ _ Hl) as (?&?&?). eauto.
 Qed.
 
-- 
GitLab