pub broadcast proof fn axiom_spec_len<T, A: Allocator>(v: &VecDeque<T, A>)
#[trigger] spec_vec_dequeue_len(v) == v@.len(),