diff --git a/coq-lifetime-logic.opam b/coq-lifetime-logic.opam
index 06d9ad5680838fd9f3dd7984729da1c7775d6c1d..31e8c5afed7d838fab00dfec3fb35225d546119f 100644
--- a/coq-lifetime-logic.opam
+++ b/coq-lifetime-logic.opam
@@ -12,7 +12,7 @@ The lifetime logic extends Iris with a notion of "borrowing".
 """
 
 depends: [
-  "coq-iris" { (= "dev.2024-09-05.0.f6ed0921") | (= "dev") }
+  "coq-iris" { (= "dev.2024-09-10.0.f14ebfde") | (= "dev") }
 ]
 
 build: ["./make-package" "lifetime" "-j%{jobs}%"]
diff --git a/lambda-rust/typing/soundness.v b/lambda-rust/typing/soundness.v
index 11c4e6989217d52506a702747c92abdeeb840537..2a1dc75684f616fda2b30fd5a9c4c61c2c38e53b 100644
--- a/lambda-rust/typing/soundness.v
+++ b/lambda-rust/typing/soundness.v
@@ -53,7 +53,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.