Function u16_be_to_bytes 

pub open spec fn u16_be_to_bytes(o: u16) -> [u8; 2]

{ [((o >> 8) & 0xff) as u8, (o & 0xff) as u8] }