Function lemma_byte_array_view 

pub broadcast proof fn lemma_byte_array_view<const N: usize>(bytes: &[u8; N])

ensures

#[trigger] bytes.deep_view() == bytes@,

Fixed byte arrays have the same shallow and deep views.