diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index a63c781e549ae30ce5ff216dfc080e3161396de6..2d33a2f800a4869eaa041463bc3e0a0da2334211 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-07-23.0.bc8c3ad9") | (= "dev") }
+  "coq-gpfsl" { (= "dev.2021-07-27.0.774a97d1") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/lifetime/model/creation.v b/theories/lifetime/model/creation.v
index ba52c8bec7f1428fd14d7c91ceae273b8f3b92a7..51ab71b8db4991ad70d4ca892e1d0439dfb777e8 100644
--- a/theories/lifetime/model/creation.v
+++ b/theories/lifetime/model/creation.v
@@ -244,8 +244,8 @@ Proof.
   assert (Hhv : ∀ κ, κ ∈ dom (gset _) I → lft_has_view A' κ (Vs κ)).
   { intros κ Hκ Λ' HΛ'. assert (Hhv : lft_has_view A κ (Vs κ)) by auto.
     specialize (Hhv Λ' HΛ').
-    destruct (decide (Λ = Λ')) as [<-|]; rewrite ?lookup_insert ?lookup_insert_ne //=.
-    assert ({[Λ]} ⊆ κ) by by apply gmultiset_elem_of_singleton_subseteq. auto. }
+    destruct (decide (Λ =  Λ')) as [<-|]; rewrite ?lookup_insert ?lookup_insert_ne //=.
+    assert ({[Λ]} ⊆ κ) by by apply gmultiset_singleton_subseteq_l. auto. }
   iModIntro. iModIntro. iExists A', I.
   rewrite /own_alft_auth /to_alftUR fmap_insert. iFrame "HA HI".
   rewrite HI !big_sepS_union //. iSplitL "HinvD".