Function axiom_smallvec_from_iter_ensures 

pub broadcast proof fn axiom_smallvec_from_iter_ensures<A: Array>(
    remaining: Seq<A::Item>,
    s: SmallVec<A>,
)

ensures

obeys_smallvec_array::<A>()
    ==> #[trigger] FromIteratorSpec::from_iter_ensures(remaining, s)
        == (remaining == smallvec_view(&s)),

Collecting a terminated iterator into a SmallVec yields exactly its remaining elements, in order. Stated as an axiom because the orphan rule (E0117) prevents implementing FromIteratorSpecImpl for SmallVec here.