update dependencies

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

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.