Function lemma_u16_be_bytes_roundtrip 

pub broadcast proof fn lemma_u16_be_bytes_roundtrip(i: [u8; 2])

ensures

#[trigger] u16_be_to_bytes(u16_be_from_bytes(i)) == i,