Function i32_be_to_bytes 

pub open spec fn i32_be_to_bytes(o: i32) -> [u8; 4]

{ u32_be_to_bytes(o as u32) }