Function tracked_borrow 

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

requires

0 <= i < s.len(),

ensures

t == s[i],