Function axiom_smallvec_index_req 

pub broadcast proof fn axiom_smallvec_index_req<A: Array>(v: &SmallVec<A>, index: usize)

requires

obeys_smallvec_array::<A>(),

ensures

<SmallVec<A> as vstd::std_specs::core::IndexSpec<usize>>::index_req(v, &index)
    == (index < smallvec_view(v).len()),

SmallVec’s single-position indexing precondition is the slice bounds check.