update dependencies

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}%"]

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.