Function extern_spec_T__slice_T_split_first_mut 

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

extern spec for slice<T>::split_first_mut

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

terminates

ghost

ensures

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