Function axiom_spec_into_iter_borrowed Copy item path

pub broadcast proof fn axiom_spec_into_iter_borrowed<T, A: Allocator>(v: &Vec<T, A>)

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