Function axiom_smallvec_from_iter_ensures 

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

ensures

obeys_smallvec_array::<A>()
    ==> #[trigger] FromIteratorSpec::from_iter_ensures(remaining, produces, s)
        == (produces.len() == remaining.len() && produces.all(|p: bool| p)
            && 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.