pub broadcast proof fn lemma_smallvec_array_atomic_u64_2()Expand description
ensures
#[trigger] obeys_smallvec_array::<[AtomicU64; 2]>(),The [AtomicU64; 2] used by AtomicCpuSet is a well-formed SmallVec
backing store. Its concrete layout declarations above are checked by rustc.