HOL-Types_To_Sets.T2_Spaces