Function axiom_array_from_seq 

pub broadcast proof fn axiom_array_from_seq<const N: usize, T>(s: Seq<T>)

requires

s.len() == N,

ensures

(#[trigger] array_from_seq::<N, T>(s))@ == s,