pub open spec fn array_view<T, const N: usize>(a: [T; N]) -> Seq<T>
{ Seq::new(N as nat, |i: int| array_index(a, i)) }