To make this happen, you'd probably need to convert the code to equivalent C++ with vector.at(), and file an issue in the LLVM project. Maybe there is one already.
There will always be things that you can know are true but aren't provable by the compiler. In a case like this, where the relevant invariants are guaranteed by the code around it, I'd have no reservations about using unsafe and get_unchecked(_mut) to remove the spurious bounds checks. After all, that's what it's for: to tell the compiler "I know you can't prove it, but trust me."
In my code where I can't invent a sufficiently readable trick to help the compiler remove the bound tests, I keep them in most cases, because I like Rust memory safety. Eventually we'll have built-in ergonomic ways to prove Rust that some index is in bound, some value is nonzero, etc (a promising way seems this one to me: https://github.com/google/wuffs ).