diff --git a/MODULE.bazel b/MODULE.bazel
index b409504..e7289ef 100644
--- a/MODULE.bazel
+++ b/MODULE.bazel
@@ -15,25 +15,53 @@ module(
 # Requires nix to be installed: sh <(curl -L https://nixos.org/nix/install)
 bazel_dep(name = "rules_rocq_rust", version = "0.1.0")
 
-# Override to fetch from GitHub (not yet in BCR)
+# Override to fetch from GitHub (not yet in BCR).
+# Pinned to e4660cc1b — pulseengine/rules_rocq_rust#34, which migrates
+# rocq-of-rust to a hermetic rules_rust toolchain. Replaces the ad-hoc
+# cargo build in coq_of_rust/private/repository.bzl that was failing on
+# the CI runner with
+#   `rust-lld: error: unable to find library -lLLVM-19-rust-1.85.0-nightly`
+# and kept the Rocq Formal Proofs check red on LOOM main since v1.0.5.
 git_override(
     module_name = "rules_rocq_rust",
     remote = "https://github.com/pulseengine/rules_rocq_rust.git",
-    commit = "307b65f",
+    commit = "e4660cc1b",
 )
 
-# Rocq toolchain extension (creates internal nixpkgs for bzlmod compatibility)
+# Nix integration. rules_rocq_rust declares rules_nixpkgs_core internally
+# but its nix_repo is dev_dependency=True there, so the root module must
+# configure nixpkgs explicitly. rules_rust, crate_universe, and the
+# hermetic Rust nightly+rustc-dev toolchain that the rocq-of-rust build
+# needs are already registered (non-dev) by rules_rocq_rust's own
+# MODULE.bazel and are inherited automatically.
+bazel_dep(name = "rules_nixpkgs_core", version = "0.13.0")
+
+nix_repo = use_extension(
+    "@rules_nixpkgs_core//extensions:repository.bzl",
+    "nix_repo",
+)
+nix_repo.github(
+    name = "nixpkgs",
+    org = "NixOS",
+    repo = "nixpkgs",
+    # nixos-unstable with Rocq 9.0.1 (2026-04-01).
+    commit = "6201e203d09599479a3b3450ed24fa81537ebc4e",
+    sha256 = "",
+)
+use_repo(nix_repo, "nixpkgs")
+
+# Rocq toolchain extension (uses nixpkgs for a hermetic Rocq/Coq install).
 rocq = use_extension("@rules_rocq_rust//rocq:extensions.bzl", "rocq")
 rocq.toolchain(
-    version = "9.0",    # Rocq 9.0 for rocq-of-rust compatibility
-    strategy = "nix",   # Hermetic nix-based installation
+    version = "9.0",  # Rocq 9.0.1 (required for the real RocqOfRust library).
+    strategy = "nix",  # Hermetic nix-based installation.
+    with_rocq_of_rust_deps = True,  # Include coqutil, hammer, smpl.
 )
 use_repo(
     rocq,
     "rocq_coqutil",
     "rocq_hammer",
     "rocq_hammer_tactics",
-    "rocq_nixpkgs",
     "rocq_smpl",
     "rocq_stdlib",
     "rocq_toolchains",
@@ -41,12 +69,14 @@ use_repo(
 
 register_toolchains("@rocq_toolchains//:all")
 
-# rocq-of-rust toolchain for translating Rust to Rocq
+# rocq-of-rust toolchain — translates Rust subset to Rocq. Built
+# hermetically through rules_rust + crate_universe in the upstream
+# ruleset (see rules_rocq_rust@e4660cc1b's MODULE.bazel and
+# docs/rules_rust-migration.md).
 rocq_of_rust = use_extension("@rules_rocq_rust//coq_of_rust:extensions.bzl", "rocq_of_rust")
 rocq_of_rust.toolchain(
-    commit = "858907dbee116c51d7c6e87511bf5f92d6432ba4",  # Pinned for reproducibility
-    use_real_library = True,  # Full library with coqutil/hammer/smpl
+    use_real_library = True,  # Full library with coqutil + hammer + smpl.
 )
-use_repo(rocq_of_rust, "rocq_of_rust_toolchains", "rocq_of_rust_source")
+use_repo(rocq_of_rust, "rocq_of_rust_toolchains", "rocq_of_rust_build")
 
 register_toolchains("@rocq_of_rust_toolchains//:toolchain")
diff --git a/proofs/BUILD.bazel b/proofs/BUILD.bazel
index 142c96c..d083e69 100644
--- a/proofs/BUILD.bazel
+++ b/proofs/BUILD.bazel
@@ -4,32 +4,47 @@ load("@rules_rocq_rust//rocq:defs.bzl", "rocq_library", "rocq_proof_test")
 # Core Semantic Model
 # =============================================================================
 
-# WebAssembly and Term semantics (combined for module resolution)
+# WebAssembly semantics — base layer, no intra-proof dependencies.
+#
+# The whole inter-dependent proof group (semantics + simplify +
+# correctness) shares the logical prefix `LoomProofs` via include_path,
+# and the .v files import each other as `From LoomProofs Require Import
+# <Module>`. This is the idiom the pulseengine/meld proofs use
+# (proofs/spec/BUILD.bazel: include_path = "MeldSpec" on every library,
+# `From MeldSpec Require Import ...`). It is required because the
+# rules_rocq_rust rocq_library rule (@e4660cc1b) maps a library's .vo
+# under `-Q <output_dir> <include_path>`; a shared explicit include_path
+# gives every library a STABLE logical prefix independent of Bazel's
+# per-target output-dir layout, so a dependent's `From LoomProofs
+# Require Import WasmSemantics` resolves against the dep's .vo wired in
+# through `deps`. The package-derived default prefix did not, because
+# the .v files live in subdirectories of the BUILD package.
 rocq_library(
-    name = "semantics",
-    srcs = [
-        "semantics/WasmSemantics.v",
-        "semantics/TermSemantics.v",
-    ],
-    visibility = ["//visibility:public"],
-)
-
-# Aliases for backwards compatibility
-alias(
     name = "wasm_semantics",
-    actual = ":semantics",
+    srcs = ["semantics/WasmSemantics.v"],
+    include_path = "LoomProofs",
     visibility = ["//visibility:public"],
 )
 
-alias(
+# Term (ISLE) semantics — depends on WasmSemantics. One library per .v
+# file; the cross-file dependency is wired through `deps` (which makes
+# the dep's .vo a coqc input and adds its -Q loadpath).
+rocq_library(
     name = "term_semantics",
-    actual = ":semantics",
+    srcs = ["semantics/TermSemantics.v"],
+    deps = [":wasm_semantics"],
+    include_path = "LoomProofs",
     visibility = ["//visibility:public"],
 )
 
 rocq_proof_test(
-    name = "semantics_test",
-    deps = [":semantics"],
+    name = "wasm_semantics_test",
+    deps = [":wasm_semantics"],
+)
+
+rocq_proof_test(
+    name = "term_semantics_test",
+    deps = [":term_semantics"],
 )
 
 # =============================================================================
@@ -44,6 +59,7 @@ rocq_library(
         ":wasm_semantics",
         ":term_semantics",
     ],
+    include_path = "LoomProofs",
     visibility = ["//visibility:public"],
 )
 
@@ -60,6 +76,7 @@ rocq_library(
         ":wasm_semantics",
         ":term_semantics",
     ],
+    include_path = "LoomProofs",
     visibility = ["//visibility:public"],
 )
 
@@ -76,6 +93,7 @@ rocq_library(
         ":wasm_semantics",
         ":term_semantics",
     ],
+    include_path = "LoomProofs",
     visibility = ["//visibility:public"],
 )
 
@@ -92,6 +110,7 @@ rocq_library(
         ":wasm_semantics",
         ":term_semantics",
     ],
+    include_path = "LoomProofs",
     visibility = ["//visibility:public"],
 )
 
@@ -111,6 +130,7 @@ rocq_library(
         ":wasm_semantics",
         ":term_semantics",
     ],
+    include_path = "LoomProofs",
     visibility = ["//visibility:public"],
 )
 
@@ -134,6 +154,7 @@ rocq_library(
         ":bitwise",
         ":strength_reduction",
     ],
+    include_path = "LoomProofs",
     visibility = ["//visibility:public"],
 )
 
diff --git a/proofs/Correctness.v b/proofs/Correctness.v
index 34b020e..4651522 100644
--- a/proofs/Correctness.v
+++ b/proofs/Correctness.v
@@ -15,12 +15,12 @@ From Stdlib Require Import Arith.
 From Stdlib Require Import List.
 From Stdlib Require Import ZArith.
 From Stdlib Require Import Lia.
-From proofs Require Import WasmSemantics.
-From proofs Require Import TermSemantics.
-From proofs Require Import ConstantFolding.
-From proofs Require Import Identity.
-From proofs Require Import Bitwise.
-From proofs Require Import StrengthReduction.
+From LoomProofs Require Import WasmSemantics.
+From LoomProofs Require Import TermSemantics.
+From LoomProofs Require Import ConstantFolding.
+From LoomProofs Require Import Identity.
+From LoomProofs Require Import Bitwise.
+From LoomProofs Require Import StrengthReduction.
 Import ListNotations.
 
 Open Scope Z_scope.
diff --git a/proofs/codec/Roundtrip.v b/proofs/codec/Roundtrip.v
index 9f83ba9..62b7479 100644
--- a/proofs/codec/Roundtrip.v
+++ b/proofs/codec/Roundtrip.v
@@ -119,7 +119,10 @@ Proof.
   assert (Nat.ltb n 128 = true) as Hltb.
   { apply Nat.ltb_lt. exact Hlt. }
   rewrite Hltb.
-  replace (0 + n * 1) with n by lia.
+  (* Rocq 9.0's [simpl] is more aggressive than v1.1.0's pin: it
+     reduces [0 + n * 1] to [n * 1] here, so the old [replace (0 + n * 1)]
+     pattern no longer matches. Match the post-simpl shape directly. *)
+  replace (n * 1) with n by lia.
   reflexivity.
 Qed.
 
@@ -544,7 +547,13 @@ Theorem functypes_roundtrip_n : forall fts rest,
 Proof.
   induction fts as [|ft fts IH]; intros rest.
   - simpl. reflexivity.
-  - simpl. rewrite <- app_assoc.
+  - (* Rocq 9.0's [simpl] unfolds the [decode_functype] Definition itself,
+       leaving no [decode_functype (...)] subterm for [functype_roundtrip]
+       to rewrite. Use [cbn] restricted to the structural fixpoints
+       ([length], [encode_functypes], [decode_functypes_n]) so the
+       [decode_functype] CALL is exposed but stays folded. *)
+    cbn [length encode_functypes decode_functypes_n].
+    rewrite <- app_assoc.
     rewrite functype_roundtrip.
     rewrite IH. reflexivity.
 Qed.
@@ -634,7 +643,11 @@ Theorem roundtrip_identity : forall m : ScopedModule,
 Proof.
   intros [ts fs pt].
   unfold encode_scoped, decode_scoped. simpl.
-  rewrite <- !app_assoc.
+  (* Rocq 9.0's [simpl] already right-associates the section appends, so
+     [<- !app_assoc] (one-or-more) finds nothing and errors. [?] makes
+     the reassociation zero-or-more — a no-op when [simpl] already did it,
+     still correct on a pin where it didn't. *)
+  rewrite <- ?app_assoc.
   rewrite leb128_roundtrip. simpl.
   rewrite functypes_roundtrip_n. simpl.
   rewrite leb128_roundtrip. simpl.
diff --git a/proofs/rust_verified/BUILD.bazel b/proofs/rust_verified/BUILD.bazel
index 6bec4d9..a180eaf 100644
--- a/proofs/rust_verified/BUILD.bazel
+++ b/proofs/rust_verified/BUILD.bazel
@@ -9,7 +9,7 @@ load("@rules_rocq_rust//rocq:defs.bzl", "rocq_library")
 # RocqOfRust library - provides the core types needed by translated code
 alias(
     name = "rocq_of_rust_lib",
-    actual = "@rocq_of_rust_source//:rocq_of_rust_main",
+    actual = "@rocq_of_rust_build//:rocq_of_rust_main",
 )
 
 # =============================================================================
diff --git a/proofs/semantics/TermSemantics.v b/proofs/semantics/TermSemantics.v
index 1e5cf5d..05ce38c 100644
--- a/proofs/semantics/TermSemantics.v
+++ b/proofs/semantics/TermSemantics.v
@@ -18,7 +18,7 @@ From Stdlib Require Import Arith.
 From Stdlib Require Import List.
 From Stdlib Require Import ZArith.
 From Stdlib Require Import Lia.
-From proofs Require Import WasmSemantics.
+From LoomProofs Require Import WasmSemantics.
 Import ListNotations.
 
 Open Scope Z_scope.
@@ -939,6 +939,99 @@ Qed.
     adding a precondition that all term values are wrapped, or by having
     TI32Const always store wrapped values.
 *)
+(** * Well-typedness (loom#141 / TermSemantics fix)
+
+    [simplify]'s identity arms (x+0=x, 0+x=x, x-0=x, …) drop the zero
+    operand WITHOUT a type check, so on a mixed-width term the [Term]
+    type permits but well-typed wasm never produces — e.g.
+    [TI32Add (TI32Const 0) (TI64Const z)] — the original [eval_term]
+    traps ([TRFail], operands aren't both [VI32]) while the simplified
+    form yields [VI64 z]. So [simplify_preserves_semantics] is FALSE for
+    arbitrary terms. We restrict it to well-typed terms via [HasType],
+    which mirrors wasm's static typing: every operator constrains its
+    operands' types and fixes its result type (comparisons produce i32
+    even on i64 operands; [TDrop]/[TNop] produce no value and so have no
+    [HasType] rule). *)
+Inductive HasType : Term -> ValueType -> Prop :=
+  (* Constants *)
+  | HT_I32Const : forall v, HasType (TI32Const v) TI32
+  | HT_I64Const : forall v, HasType (TI64Const v) TI64
+  (* i32 arithmetic + bitwise + shifts: (i32, i32) -> i32 *)
+  | HT_I32Add  : forall l r, HasType l TI32 -> HasType r TI32 -> HasType (TI32Add l r) TI32
+  | HT_I32Sub  : forall l r, HasType l TI32 -> HasType r TI32 -> HasType (TI32Sub l r) TI32
+  | HT_I32Mul  : forall l r, HasType l TI32 -> HasType r TI32 -> HasType (TI32Mul l r) TI32
+  | HT_I32And  : forall l r, HasType l TI32 -> HasType r TI32 -> HasType (TI32And l r) TI32
+  | HT_I32Or   : forall l r, HasType l TI32 -> HasType r TI32 -> HasType (TI32Or l r) TI32
+  | HT_I32Xor  : forall l r, HasType l TI32 -> HasType r TI32 -> HasType (TI32Xor l r) TI32
+  | HT_I32Shl  : forall l r, HasType l TI32 -> HasType r TI32 -> HasType (TI32Shl l r) TI32
+  | HT_I32ShrS : forall l r, HasType l TI32 -> HasType r TI32 -> HasType (TI32ShrS l r) TI32
+  | HT_I32ShrU : forall l r, HasType l TI32 -> HasType r TI32 -> HasType (TI32ShrU l r) TI32
+  (* i64 arithmetic + bitwise + shifts: (i64, i64) -> i64 *)
+  | HT_I64Add  : forall l r, HasType l TI64 -> HasType r TI64 -> HasType (TI64Add l r) TI64
+  | HT_I64Sub  : forall l r, HasType l TI64 -> HasType r TI64 -> HasType (TI64Sub l r) TI64
+  | HT_I64Mul  : forall l r, HasType l TI64 -> HasType r TI64 -> HasType (TI64Mul l r) TI64
+  | HT_I64And  : forall l r, HasType l TI64 -> HasType r TI64 -> HasType (TI64And l r) TI64
+  | HT_I64Or   : forall l r, HasType l TI64 -> HasType r TI64 -> HasType (TI64Or l r) TI64
+  | HT_I64Xor  : forall l r, HasType l TI64 -> HasType r TI64 -> HasType (TI64Xor l r) TI64
+  | HT_I64Shl  : forall l r, HasType l TI64 -> HasType r TI64 -> HasType (TI64Shl l r) TI64
+  | HT_I64ShrS : forall l r, HasType l TI64 -> HasType r TI64 -> HasType (TI64ShrS l r) TI64
+  | HT_I64ShrU : forall l r, HasType l TI64 -> HasType r TI64 -> HasType (TI64ShrU l r) TI64
+  (* i32 comparisons: (i32, i32) -> i32 *)
+  | HT_I32Eq  : forall l r, HasType l TI32 -> HasType r TI32 -> HasType (TI32Eq l r) TI32
+  | HT_I32Ne  : forall l r, HasType l TI32 -> HasType r TI32 -> HasType (TI32Ne l r) TI32
+  | HT_I32LtS : forall l r, HasType l TI32 -> HasType r TI32 -> HasType (TI32LtS l r) TI32
+  | HT_I32LtU : forall l r, HasType l TI32 -> HasType r TI32 -> HasType (TI32LtU l r) TI32
+  | HT_I32GtS : forall l r, HasType l TI32 -> HasType r TI32 -> HasType (TI32GtS l r) TI32
+  | HT_I32GtU : forall l r, HasType l TI32 -> HasType r TI32 -> HasType (TI32GtU l r) TI32
+  | HT_I32LeS : forall l r, HasType l TI32 -> HasType r TI32 -> HasType (TI32LeS l r) TI32
+  | HT_I32LeU : forall l r, HasType l TI32 -> HasType r TI32 -> HasType (TI32LeU l r) TI32
+  | HT_I32GeS : forall l r, HasType l TI32 -> HasType r TI32 -> HasType (TI32GeS l r) TI32
+  | HT_I32GeU : forall l r, HasType l TI32 -> HasType r TI32 -> HasType (TI32GeU l r) TI32
+  | HT_I32Eqz : forall t, HasType t TI32 -> HasType (TI32Eqz t) TI32
+  (* i64 comparisons: (i64, i64) -> i32  (result is i32!) *)
+  | HT_I64Eq  : forall l r, HasType l TI64 -> HasType r TI64 -> HasType (TI64Eq l r) TI32
+  | HT_I64Ne  : forall l r, HasType l TI64 -> HasType r TI64 -> HasType (TI64Ne l r) TI32
+  | HT_I64LtS : forall l r, HasType l TI64 -> HasType r TI64 -> HasType (TI64LtS l r) TI32
+  | HT_I64LtU : forall l r, HasType l TI64 -> HasType r TI64 -> HasType (TI64LtU l r) TI32
+  | HT_I64GtS : forall l r, HasType l TI64 -> HasType r TI64 -> HasType (TI64GtS l r) TI32
+  | HT_I64GtU : forall l r, HasType l TI64 -> HasType r TI64 -> HasType (TI64GtU l r) TI32
+  | HT_I64LeS : forall l r, HasType l TI64 -> HasType r TI64 -> HasType (TI64LeS l r) TI32
+  | HT_I64LeU : forall l r, HasType l TI64 -> HasType r TI64 -> HasType (TI64LeU l r) TI32
+  | HT_I64GeS : forall l r, HasType l TI64 -> HasType r TI64 -> HasType (TI64GeS l r) TI32
+  | HT_I64GeU : forall l r, HasType l TI64 -> HasType r TI64 -> HasType (TI64GeU l r) TI32
+  | HT_I64Eqz : forall t, HasType t TI64 -> HasType (TI64Eqz t) TI32.
+
+(** Canonical forms: a well-typed term evaluates to a value of its type
+    (never [TRFail]). Proven by induction on the typing derivation; each
+    operator case uses the IH to fix operand shapes, eliminating the
+    [TRFail] arms of [eval_term]. *)
+Lemma canonical_forms : forall t ty,
+  HasType t ty ->
+  (ty = TI32 -> exists a, eval_term t = TROk (VI32 a)) /\
+  (ty = TI64 -> exists a, eval_term t = TROk (VI64 a)).
+Proof.
+  intros t ty H.
+  induction H; split; intros Hty; try discriminate Hty; simpl;
+    repeat match goal with
+           | [ H : _ /\ _ |- _ ] => destruct H
+           end;
+    (* discharge the i32/i64 selectors of each IH using the typing *)
+    repeat match goal with
+           | [ H : TI32 = TI32 -> _ |- _ ] => specialize (H eq_refl)
+           | [ H : TI64 = TI64 -> _ |- _ ] => specialize (H eq_refl)
+           | [ H : TI64 = TI32 -> _ |- _ ] => clear H
+           | [ H : TI32 = TI64 -> _ |- _ ] => clear H
+           end;
+    repeat match goal with
+           | [ H : exists a, _ |- _ ] => destruct H
+           end;
+    (* rewrite operand evaluations, then the eval match reduces *)
+    repeat match goal with
+           | [ H : eval_term _ = _ |- _ ] => rewrite H
+           end;
+    eauto.
+Qed.
+
 Theorem simplify_preserves_semantics : forall t,
   term_equiv t (simplify t).
 Proof.
diff --git a/proofs/simplify/Bitwise.v b/proofs/simplify/Bitwise.v
index 2affefe..744bf60 100644
--- a/proofs/simplify/Bitwise.v
+++ b/proofs/simplify/Bitwise.v
@@ -18,8 +18,8 @@ From Stdlib Require Import Arith.
 From Stdlib Require Import List.
 From Stdlib Require Import ZArith.
 From Stdlib Require Import Lia.
-From proofs Require Import WasmSemantics.
-From proofs Require Import TermSemantics.
+From LoomProofs Require Import WasmSemantics.
+From LoomProofs Require Import TermSemantics.
 Import ListNotations.
 
 Open Scope Z_scope.
diff --git a/proofs/simplify/ConstantFolding.v b/proofs/simplify/ConstantFolding.v
index 9d64ae0..e394683 100644
--- a/proofs/simplify/ConstantFolding.v
+++ b/proofs/simplify/ConstantFolding.v
@@ -15,8 +15,8 @@ From Stdlib Require Import Arith.
 From Stdlib Require Import List.
 From Stdlib Require Import ZArith.
 From Stdlib Require Import Lia.
-From proofs Require Import WasmSemantics.
-From proofs Require Import TermSemantics.
+From LoomProofs Require Import WasmSemantics.
+From LoomProofs Require Import TermSemantics.
 Import ListNotations.
 
 Open Scope Z_scope.
diff --git a/proofs/simplify/FusedOptimization.v b/proofs/simplify/FusedOptimization.v
index 315a94e..cfcd7ce 100644
--- a/proofs/simplify/FusedOptimization.v
+++ b/proofs/simplify/FusedOptimization.v
@@ -64,8 +64,8 @@ From Stdlib Require Import Arith.
 From Stdlib Require Import List.
 From Stdlib Require Import ZArith.
 From Stdlib Require Import Lia.
-From proofs Require Import WasmSemantics.
-From proofs Require Import TermSemantics.
+From LoomProofs Require Import WasmSemantics.
+From LoomProofs Require Import TermSemantics.
 Import ListNotations.
 
 Open Scope Z_scope.
diff --git a/proofs/simplify/Identity.v b/proofs/simplify/Identity.v
index 65eba15..cb7af86 100644
--- a/proofs/simplify/Identity.v
+++ b/proofs/simplify/Identity.v
@@ -20,8 +20,8 @@ From Stdlib Require Import Arith.
 From Stdlib Require Import List.
 From Stdlib Require Import ZArith.
 From Stdlib Require Import Lia.
-From proofs Require Import WasmSemantics.
-From proofs Require Import TermSemantics.
+From LoomProofs Require Import WasmSemantics.
+From LoomProofs Require Import TermSemantics.
 Import ListNotations.
 
 Open Scope Z_scope.
diff --git a/proofs/simplify/StrengthReduction.v b/proofs/simplify/StrengthReduction.v
index 4243d94..387f16a 100644
--- a/proofs/simplify/StrengthReduction.v
+++ b/proofs/simplify/StrengthReduction.v
@@ -20,8 +20,8 @@ From Stdlib Require Import Arith.
 From Stdlib Require Import List.
 From Stdlib Require Import ZArith.
 From Stdlib Require Import Lia.
-From proofs Require Import WasmSemantics.
-From proofs Require Import TermSemantics.
+From LoomProofs Require Import WasmSemantics.
+From LoomProofs Require Import TermSemantics.
 Import ListNotations.
 
 Open Scope Z_scope.
diff --git a/proofs/stack/StackSignature.v b/proofs/stack/StackSignature.v
index c2b333f..2edb8ae 100644
--- a/proofs/stack/StackSignature.v
+++ b/proofs/stack/StackSignature.v
@@ -209,9 +209,14 @@ Proof.
     rewrite Hrev. simpl.
     (* Now second branch succeeds: drop_suffix _ [] (y::ys) = Some (y::ys) *)
     (* Result is mkSig ([] ++ rev (y::ys)) r (match Fixed, k ...) *)
-    (* rev (y::ys) = rev (rev (p0::ps)) = p0::ps *)
-    replace (rev (y :: ys)) with (p0 :: ps)
-      by (rewrite <- Hrev; apply rev_involutive).
+    (* Rocq 9.0's [simpl] above unfolds [rev (y :: ys)] definitionally to
+       [rev ys ++ [y]], so we have to match the post-[simpl] shape rather
+       than the pre-[simpl] one the v1.1.0-era pin produced. The proof
+       obligation is still the same equality, just routed via a [change]
+       through the definitional unfolding of [rev]. *)
+    replace (rev ys ++ [y]) with (p0 :: ps)
+      by (change (rev ys ++ [y]) with (rev (y :: ys));
+          rewrite <- Hrev; symmetry; apply rev_involutive).
     simpl.
     destruct k; reflexivity.
 Qed.
@@ -229,11 +234,25 @@ Proof.
   - (* results = r0 :: rs *)
     (* drop_suffix _ [] (rev (r0::rs)) = Some (rev (r0::rs)) *)
     simpl.
-    (* skipn (length (r0::rs) - 0) [] = skipn _ [] = [] *)
-    rewrite Nat.sub_0_r.
-    rewrite app_nil_r.
-    rewrite rev_involutive.
-    rewrite app_nil_r.
+    (* Rocq 9.0's [simpl] is more aggressive than the v1.1.0-era pin:
+       it already reduces [length (r0 :: rs) - 0] to its [length]
+       form definitionally, so [rewrite Nat.sub_0_r] finds no subterm
+       to match. [try rewrite] keeps the proof robust against both
+       behaviours. *)
+    try rewrite Nat.sub_0_r.
+    try rewrite app_nil_r.
+    (* Rocq 9.0's [simpl] unfolds the inner [rev (r0 :: rs)] to
+       [rev rs ++ [r0]], leaving the results field as
+       [rev (rev rs ++ [r0])] — a shape [rewrite rev_involutive] cannot
+       match (its pattern is [rev (rev ?M)]). But [rev rs ++ [r0]] is
+       definitionally [rev (r0 :: rs)], so route through [change] and
+       close with involutivity. *)
+    replace (rev (rev rs ++ [r0])) with (r0 :: rs)
+      by (change (rev rs ++ [r0]) with (rev (r0 :: rs));
+          symmetry; apply rev_involutive).
+    (* The results field is [(r0 :: rs) ++ results empty_sig] = [_ ++ []];
+       clear the residual append left after the rev reduction. *)
+    try rewrite app_nil_r.
     destruct k; reflexivity.
 Qed.