pub broadcast proof fn axiom_spec_array_as_slice<T, const N: usize>(ar: &[T; N])
(#[trigger] spec_array_as_slice(ar))@ == ar@,