Function obeys_smallvec_array 

pub open spec fn obeys_smallvec_array<A: Array>() -> bool

{
    size_of::<A>() == smallvec_array_size::<A>() * size_of::<A::Item>()
        && align_of::<A>() >= align_of::<A::Item>()
}

Whether A is a well-formed standard Array impl, i.e. smallvec’s SmallVec::new construction assert holds: the reported element count and the alignment of A are consistent with the real layouts of A and A::Item. The two array instances used by OSTD satisfy this guard via the concrete lemmas below; any other impl needs corresponding layout and size facts.