Unexpected error "Verus currently only supports casts from integer types"

[jonhnet]

I have a pile of code that compiles and verifies fine. I modified a data structure to have a borrowed field and a lifetime parameter, and an apparently unrelated method in that struct now throws this error:

error: Verus currently only supports casts from integer types and `char` to integer types
   --> src/marshalling/VariableSizedElementSeq_v.rs:725:60
    |
725 |                     forall |ip, jp| 0 <= ip <= jp <= i ==> tbl[jp] as int <= tbl[ip] as int
    |                                

I have no idea how it has anything to do with the change I made.

Recording:
2024-09-19-09-19-54.zip