pub proof fn tracked_borrow_mut_slice<T, A: Allocator>(
tracked vec: &mut Vec<T, A>,
) -> tracked t : &mut [T]Expand description
ensures
(*t)@ == old(vec)@,(*t).len() == final(t).len(),final(vec)@ == final(t)@,