Function axiom_spec_array_iter Copy item path

pub broadcast proof fn axiom_spec_array_iter<T, const N: usize>(s: &[T; N])

#[trigger] spec_array_iter(s).remaining() == s@.as_ref(),