Function generic_slice_index_mut_postcondition 

pub open spec fn generic_slice_index_mut_postcondition<R: RangeBoundsSpec<usize>, T>(
    range: &R,
    old_slice: Seq<T>,
    final_slice: Seq<T>,
    immediate_output: Seq<T>,
    final_output: Seq<T>,
) -> bool

{
    &&& immediate_output
        == old_slice[slice_range_start(range)..slice_range_end(range, old_slice.len())]
    &&& final_slice.len() == old_slice.len()
    &&& final_slice[..slice_range_start(range)] == old_slice[..slice_range_start(range)]
    &&& final_slice[slice_range_start(range)..slice_range_end(range, old_slice.len())]
        == final_output
    &&& final_slice[slice_range_end(range, old_slice.len())..old_slice.len()]
        == old_slice[slice_range_end(range, old_slice.len())..old_slice.len()]
    &&& final_slice
        == old_slice[..slice_range_start(range)] + final_output
            + old_slice[slice_range_end(range, old_slice.len())..old_slice.len()]

}