pub broadcast proof fn axiom_spec_array_fill_for_copy_type<T: Copy, const N: usize>(t: T)Expand description
ensures
forall |i: int| 0 <= i < N ==> spec_array_fill_for_copy_type::<T, N>(t).view()[i] == t,