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