Requested feature: loop_old similar to old that can refers to historic values in loop contracts
Use case:

#[kani::loop_invariants(loop_old(x) == y)]

where loop_old(x) refers to the value of x upon the entrance of the loop.
Link to relevant documentation (Rust reference, Nomicon, RFC): #3167

Test case:

let mut x: u8 = kani::any_where(|v| *v < 10);
let mut y: u8 = kani::any();
let mut i = 0;
#[kani::loop_invariants(i == 0 || loop_old(x) == y)]
while i < 5{
  if i == 0{
    y = x
  }
  x += 1;
  i += 1;
}