Function spec_slice_ends_with 

pub open spec fn spec_slice_ends_with<T: PartialEq>(slice: &[T], needle: &[T]) -> bool

{
    &&& needle@.len() <= slice@.len()
    &&& forall |i: int| {
        0 <= i < needle@.len()
            ==> <T as super::cmp::PartialEqSpec<
                T,
            >>::eq_spec(&slice@[slice@.len() - needle@.len() + i], &needle@[i])
    }

}