update dependencies

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}%"]

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.