pub broadcast proof fn axiom_array_ext_equal<T, const N: usize>(a1: [T; N], a2: [T; N])Expand description
ensures
#[trigger] (a1 =~= a2) <==> (forall |i: int| 0 <= i < N ==> a1[i] == a2[i]),