Support for dependent case analysis #32
Description
Currently, there is no way to do case analysis on an indexed datatype whose indices are not fully general (well, technically there is nothing enforcing full generality, but that is only because of #31). To support proper dependent case analysis, we need to support specialization by unification. This could be built into the typing of case statements, but it could also be its own term constructor that does just the specialization, which might make for a nicer presentation of the typing rules.