Function lemma_smallvec_array_u64_2 

pub broadcast proof fn lemma_smallvec_array_u64_2()

ensures

#[trigger] obeys_smallvec_array::<[u64; 2]>(),

The [u64; 2] used by CpuSet is a well-formed SmallVec backing store. Its concrete layout declarations above are checked by rustc.