Function str_slice_index_postcondition 

pub open spec fn str_slice_index_postcondition<R: RangeBoundsSpec<usize>>(
    range: &R,
    s: Seq<u8>,
    r: Seq<u8>,
) -> bool

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