Function spec_slice_index Copy item path

pub uninterp fn spec_slice_index<T>(slice: &[T], i: int) -> T