The call define_finite_type n where n is a positive integer defines a new
type also called simply `n', and returns a theorem asserting that its
universe has size n, in the form:
|- (:n) HAS_SIZE n
where (:n) is the customary HOL Light printing of the universe set
UNIV:n->bool.
FAILURE CONDITIONS
Fails if n is zero or negative, or if there is a type of the same name
(unless it was also defined by the same call for define_finite_type, which is
perfectly permissible), or if the names of the type constructor and destructor
functions are already in use: