Function str_slice_index_mut_postcondition 

pub open spec fn str_slice_index_mut_postcondition<R: RangeBoundsSpec<usize>>(
    range: &R,
    old_s: Seq<u8>,
    final_s: Seq<u8>,
    r: Seq<u8>,
    final_r: Seq<u8>,
) -> bool

{
    let start = slice_range_start(range);
    let end = slice_range_end(range, old_s.len());
    &&& r == old_s[start..end]
    &&& final_s.len() == old_s.len()
    &&& final_s[..start] == old_s[..start]
    &&& final_s[start..end] == final_r
    &&& final_s[end..old_s.len()] == old_s[end..]

}