Type Alias EverCrypt_Helpers_uint16_t 

pub type EverCrypt_Helpers_uint16_t = u16;