Normalization can pull in named regions from the parameter
environment. We need to be prepared for that in the opaque
types code.

We now make `'empty` indexed by a universe index, resulting
in a region lattice like this:

```
static ----------+-----...------+       (greatest)
|                |              |
early-bound and  |              |
free regions     |              |
|                |              |
scope regions    |              |
|                |              |
empty(root)   placeholder(U1)   |
|            /                  |
|           /         placeholder(Un)
empty(U1) --         /
|                   /
...                /
|                 /
empty(Un) --------                      (smallest)
```

Therefore, `exists<A> { forall<B> { B: A } }` is now unprovable,
because A must be at least Empty(U1) and B is placeholder(U2), and hence
the two regions are unrelated.