Function spec_slice_contains 

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

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