Function tracked_borrow_mut 

pub proof fn tracked_borrow_mut<T>(tracked s: &mut [T], i: int) -> tracked t : &mut T

requires

0 <= i < s.len(),

ensures

*t == old(s)[i],

final(s)@ == old(s)@.update(i, *final(t)),