Semantic change: I always consider a type with no constructors as an empty

Semantic change: I always consider a type with no constructors as an empty
type even if it is mutually recursive with non-empty types. I think that
this should be a sound generalization.

Note: Coq assumes a type to be empty iff it is not mutually recursive with
any other inductive type.