Typechecking fails for eliminations of values of computed types

[robrix]

For example, the Branches function in #172 computes a type as either a (right-nested) Pair or Unit (terminating the list). But if we take a value of that type and try to eliminate it by use of first, it won’t work; there’s no way for definitional equality to reduce the call to Branches to determine the actual type.

We might be able to work around this by the addition of eliminators specific to values typed by Branches, but in general it appears that our definitional equality isn’t strong enough.