pub trait ExSliceIndex<T>where
T: ?Sized,{
type ExternalTraitSpecificationFor: SliceIndex<T>;
type Output: ?Sized;
// Required methods
spec fn index_req(&self, slice: &T) -> bool;
exec fn index(self, slice: &T) -> &Self::Output;
}