HOL-Types_To_Sets.Types_To_Sets