Function axiom_spec_iter Copy item path

pub broadcast proof fn axiom_spec_iter<'a, T, A: Allocator>(v: &'a VecDeque<T, A>)

#[trigger] spec_iter(v).remaining() == v@.as_ref(),