Function axiom_array_decreases_to_seq 

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

ensures

#[trigger] (decreases_to!(a => a @)),

We axiomatize that an array can decrease to its corresponding sequence.