Function i16_be_from_bytes 

pub open spec fn i16_be_from_bytes(i: [u8; 2]) -> i16

{ u16_be_from_bytes(i) as i16 }