Right now you can't use `<|>` without also having to admit the `empty` case. We should split it up.
Right now you can't use
<|>without also having to admit theemptycase. We should split it up.