Function extern_spec_T__slice_T_split_off_first_mut 

pub fn extern_spec_T__slice_T_split_off_first_mut<'a, T>(
    self_: &mut &'a mut [T],
) -> Option<&'a mut T>

extern spec for slice<T>::split_off_first_mut

This is not a real function: its only use is for documentation.

terminates

ghost

ensures

match result {
    Some(r) => {
        *r == (**self)[0] && ^r == (^*self)[0] &&
        (**self)@.len() > 0 && (^*self)@.len() > 0 &&
        (*^self)@ == (**self)@.tail() && (^^self)@ == (^*self)@.tail()
    }
    None => (*^self)@ == Seq::empty() && (^*self)@ == Seq::empty() &&
            (**self)@ == Seq::empty() && (^^self)@ == Seq::empty()
}