Function i16_be_to_bytes 

pub open spec fn i16_be_to_bytes(o: i16) -> [u8; 2]

{ u16_be_to_bytes(o as u16) }