pub proof fn tracked_borrow_slice<T, A: Allocator>(tracked vec: &Vec<T, A>) -> tracked t : &[T]
t@ == vec@,