Function i16_le_from_bytes 

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

{ u16_le_from_bytes(i) as i16 }