Function lemma_byte_slice_view 

pub broadcast proof fn lemma_byte_slice_view(bytes: &[u8])

ensures

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

Byte slices have the same shallow and deep views.