diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index 1a16b6ab325e96befb066e829b36d4e12eedeca5..aed9d929e0d4be7a2b07ed4933dc787af0b548eb 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.2023-10-03.0.41e501bd") | (= "dev") }
+  "coq-gpfsl" { (= "dev.2023-10-14.0.18d22854") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/lifetime/model/faking.v b/theories/lifetime/model/faking.v
index 4c7d0168ead883c4f32b3b8215e80238ad894150..62b7420b92376499310bd90324f99b85f48f8531 100644
--- a/theories/lifetime/model/faking.v
+++ b/theories/lifetime/model/faking.v
@@ -57,8 +57,7 @@ Proof.
     { intros Λ. rewrite lookup_op lookup_gset_to_gmap !lookup_fmap lookup_union_with
         lookup_gset_to_gmap.
       destruct (A !! Λ) eqn:EQ.
-      - apply elem_of_dom_2 in EQ.
-        rewrite [X in _ ≡ X ⋅ _]option_guard_False; last set_solver. by destruct mguard.
+      - apply elem_of_dom_2 in EQ. repeat case_guard; set_solver.
       - apply not_elem_of_dom in EQ.
         destruct (decide (Λ ∈ dom κ)).
         + rewrite !option_guard_True; set_solver.