Bottoms are ignored for this entire module: only fully-defined inhabitants are considered inhabitants.
Creating an instance of this class is a declaration that your type is
recursively enumerable (and that
universe is that enumeration). In
particular, you promise that any finite inhabitant has a finite index in
universe, and that no inhabitant appears at two different finite indices.
Creating an instance of this class is a declaration that your
eventually ends. Minimal definition: no methods defined. By default,
universeF = universe, but for some types (like
method may have a more intuitive ordering.