Function lemma_array_from_seq_roundtrip 

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

ensures

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