On type-cases, union elimination, and occurrence typing.