Function generic_slice_index_postcondition 

pub open spec fn generic_slice_index_postcondition<R: RangeBoundsSpec<usize>, T>(
    range: &R,
    slice: Seq<T>,
    r: Seq<T>,
) -> bool

{ r == slice[slice_range_start(range)..slice_range_end(range, slice.len())] }