Function slice_subrange 

pub exec fn slice_subrange<'a, T>(slice: &'a [T], i: usize, j: usize) -> out : &'a [T]

requires

0 <= i <= j <= slice@.len(),

ensures

out@ == slice@[i..j],