diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index e0bfe4f8d966e7d580ec3b508a6183b9bc4fdf8c..c325151bfecf4089abb84f06b4094e25602d07fb 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.2024-09-10.0.6170a8bd") | (= "dev") }
+  "coq-gpfsl" { (= "dev.2024-09-10.1.5365229f") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/typing/soundness.v b/theories/typing/soundness.v
index 5f77054ec0c121a0f2348b631f43a7628cc19a38..e95f9721eb77d76e7d982b9ce83469936b6c4875 100644
--- a/theories/typing/soundness.v
+++ b/theories/typing/soundness.v
@@ -61,7 +61,6 @@ Section type_soundness.
     { by rewrite /elctx_interp /=. }
     { rewrite /llctx_interp /=. iSplit; last done. iExists ϝ.
       rewrite /= left_id. iSplit; first done.
-      rewrite decide_True //.
       by iDestruct "Hϝ" as "[$ #$]". }
     rewrite cctx_interp_singleton. simpl. iIntros (args) "_ _".
     inv_vec args. iIntros (x) "_ /=". by wp_lam.