Type Alias EverCrypt_Hash_alg13 

pub type EverCrypt_Hash_alg13 = Spec_Hash_Definitions_hash_alg;