Expected interaction for enumerated values, integer overflow, and equality

Hi!

I'm trying to use the semantics of Lustre given in this compiler to prove some properties about transformations of Lustre programs. Naively, I would expect the following two properties to hold:

1. Given an equation
`x = case y of |0 => e_0 | ... | n => e_n`
I would expect the new equation
`x = case y = 0 of | true => e_0 | false => case y = 1 of | true => e_1 | false => case y = 2...`
to be equivalent to the old one at all timesteps.

2. Given a node defined by equations
`last x = n`
`x = e when C(y)`
I would expect a node defined by
`last x = n`
`x = case (C = y) of | true => e | false => last x`
to be equivalent for values of x on timesteps where `C = y`

Due to the casting of enumerated values from `nat` to fixed length machine integers, I can't show that either property holds when the number of constructors for the enumerated type is greater than the modulus of the machine integer due to integer overflow. Is this interaction between very large enumerated types, casting for application of operators, and integer overflow accounted for somewhere in the development, and is this the desired behavior?

Apologies if this is documented somewhere and I missed it. I didn't see mention of this in any of the work published in English, and I couldn't find any lemmas related to this in the Rocq development.