Function generic_slice_in_bounds 

pub open spec fn generic_slice_in_bounds<R: RangeBoundsSpec<usize>, T>(
    range: &R,
    s: Seq<T>,
) -> bool

{ slice_range_valid(range, s.len()) }