> to prove something to the compiler that is trivially known to be true

I don't think you've ever done any serious work with lifetimes. I've been a rust developer for a number of years, and I have never once encountered a situation where the rust compiler forces me to add annotations for something which is trivially true. Never.

What actually happens is 95% of the time I never have to add lifetime annotations anyway because the compiler infers the correct annotation from the lifetime elision rules. The remaining 1 in 20 instances is when the borrow checker yells at me, and literally every single time it is due to a latent logic bug in my code. For example, accessing memory after it's been freed, or using a container after it has been consumed. Stuff that C++ would call "undefined behavior" and are generally considered Very Bad Things by C++ developers as well.

It boggles my mind that you don't want the compiler to tell you that “you have a logic error here.”