Admitted in Equations: anomaly

[louwenus]

Description of the problem

Hello.
Upon writting an Equations, I could not prove a goal due to using a with where the result was not linked to the inital argument anymore, making it impossible to deduce anything.
I the tried to use admit and Admitted, and was shown this error:

Error: Anomaly "Uncaught exception Invalid_argument("List.fold_left2")."
Please report at http://rocq-prover.org/bugs/.

NB: Here are my packages version for a few rock package (installed with opam) if it is relevant
rocq-core 9.0.1 The Rocq Prover with its prelude
rocq-elpi 3.2.0 Elpi extension language for Coq
rocq-equations 1.3.1+9.0 A function definition package for Rocq
rocq-hierarchy-builder 1.10.1 High level commands to declare and evolve a hierarchy based on packed classes
rocq-mathcomp-algebra 2.4.0 Mathematical Components Library on Algebra
rocq-mathcomp-fingroup 2.4.0 Mathematical Components Library on finite groups
rocq-mathcomp-ssreflect 2.4.0 Small Scale Reflection
rocq-prover 9.0.0 The Rocq Prover with Stdlib
rocq-runtime 9.0.1 The Rocq Prover -- Core Binaries and Tools
rocq-stdlib 9.0.0 The Rocq Proof Assistant -- Standard Library

Small Rocq / Coq file to reproduce the bug

From Equations Require Import Equations.

Equations? g (n:nat) :nat by wf n lt :=
g (S x) := g x;
g 0  := 0. 
Admitted.

Version of Rocq / Coq where this bug occurs

9.0.1

Interface of Rocq / Coq where this bug occurs

rocq compile

Last version of Rocq / Coq where the bug did not occur

No response