diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index 65c16c0e759edb7e107934a55231d354a8bc64c9..a63c781e549ae30ce5ff216dfc080e3161396de6 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-27.0.bf367fe7") | (= "dev") }
+  "coq-gpfsl" { (= "dev.2021-07-23.0.bc8c3ad9") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/lifetime/model/creation.v b/theories/lifetime/model/creation.v
index aa0f12f68cf9d5b26294ba0fed0b53897c4ac9b0..bd81be51158a279731e9b99c92b9b3e09b746d41 100644
--- a/theories/lifetime/model/creation.v
+++ b/theories/lifetime/model/creation.v
@@ -185,7 +185,6 @@ Proof.
     assert (↑mgmtN ## userE) by solve_ndisj. set_solver. }
   { done. }
   iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
-  { rewrite <-union_subseteq_l. solve_ndisj. }
   iMod (ilft_create _ _ {[+ Λ +]} with "HA HI Hinv") as "H". clear A I.
   iDestruct "H" as (A I) "(% & HA & HI & Hinv)".
   rewrite /lft_tok /= big_sepMS_singleton. iDestruct "HΛ" as (V'0) "[#HV'0 HΛ]".