Function spec_slice_starts_with 

pub open spec fn spec_slice_starts_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@[i], &needle@[i])
    }

}