Function extern_spec_T_A_VecDeque_T_A_pop_front 

pub fn extern_spec_T_A_VecDeque_T_A_pop_front<T, A: Allocator>(
    self_: &mut VecDeque<T, A>,
) -> Option<T>

extern spec for VecDeque<T, A>::pop_front

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

terminates

ghost

ensures

match result {
    Some(t) =>
        (^self)@ == self@.subsequence(1, self@.len()) &&
        self@ == (^self)@.push_front(t),
    None => *self == ^self && self@.len() == 0
}