Errors with extern_spec on SliceIndex trait

[nokunish]

use prusti_contracts::*;
use std::{alloc::Allocator, ops::Deref, slice::SliceIndex, option::Option};

#[extern_spec]
impl <T, A> Deref for Vec<T, A>
    where   A: Allocator
{
    #[pure]
    fn deref(&self) -> &Self::Target;
}

#[extern_spec]
impl<T> SliceIndex<[T]> for usize
{   
    #[pure]
    fn get(self, slice: &[T]) -> Option<&Self::Output>;
}

#[pure]
pub fn get_vec<T>(self, index: usize) -> Option<&T>
    where T: Clone,
{
    SliceIndex::get(index, &vec)
} 

Calling SliceIndex functions (tested SliceIndex::get, SliceIndex::index) from inside a pure function get_vec produces the error message: [Prusti: invalid specification] use of impure function "std::slice::SliceIndex::get" in pure code is not allowed

Interestingly though, when another pure function is called onto the result it (i.e. is_some_vec),

#[extern_spec]
impl<T> Option<T> 
{
    #[pure]
    pub fn is_some(&self) -> bool;
}

pub fn is_some_vec<T>(vec: &Vec<T>, index: usize) -> bool
{
    SliceIndex::get(index, &vec).is_some()
} 

it triggers Details: There is no procedure contract for loan bw6. This could happen if you are chaining pure functions, which is not fully supported.

There seem be inconsistency regarding Prusti's recognition of SliceIndex functions as pure.