internal error: interaction with builtin::Integer and triggers

[jonhnet]

I pulled a recent main 9711235 and got a panic on verisplinter. Recording attached.

2024-11-05-13-02-57.zip

[tjhance]

minimal repro:

proof fn test<B: builtin::Integer>(tbl: Seq<B>, i: int) {
    assert(forall |ip, jp| 0 <= ip <= jp <= i ==> tbl[jp] as int <= tbl[ip] as int);
}