diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index 48f00a75b189a5b72f3659f9568a25cc08ee27fd..0a58cdf737fa8eb8d4943f39c64bb9404838f0c4 100644
--- a/coq-lambda-rust.opam
+++ b/coq-lambda-rust.opam
@@ -15,7 +15,7 @@ This branch uses a proper weak memory model.
 """
 
 depends: [
-  "coq-gpfsl" { (= "dev.2021-06-06.0.5b953c99") | (= "dev") }
+  "coq-gpfsl" { (= "dev.2021-06-18.0.336531e4") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/lifetime/model/creation.v b/theories/lifetime/model/creation.v
index d4ed860eb42703647822c87428c2a7df751a94f8..aa0f12f68cf9d5b26294ba0fed0b53897c4ac9b0 100644
--- a/theories/lifetime/model/creation.v
+++ b/theories/lifetime/model/creation.v
@@ -206,7 +206,7 @@ Proof.
     by inversion EQ. }
   iDestruct (exists_Vs with "Hinv") as (Vs) "(>% & >% & Hinv)".
   iMod (own_update_2 with "HA HΛ") as "[HA HΛ]".
-  { destruct (equiv_Some_inv_r' _ _ Eqs) as (? & ? & ?).
+  { apply Some_equiv_eq in Eqs as (? & ? & ?).
     by eapply auth_update, singleton_local_update,
        (exclusive_local_update _ (Cinr (to_agree (to_latT (Vs {[Λ]}))))). }
   iDestruct "HΛ" as "#HΛ". iModIntro; iNext.