Decompose elim into rec and case

[jonsterling]

@ecavallo I'd like to consider decomposing the eliminators into two different combinators: case and rec, as described in here: https://cs.ru.nl/~freek/courses/tt-2010/tvftl/epigram-notes.pdf

The idea is that case doesn't do any recursion, but just lets you see what constructor you have. And rec does the recursion (basically, for each type, it takes a motive P and provides all the recursive calls that can be made).

We'd have to make sure that this idea works for HITs, but a priori I have no reason to expect that it wouldn't extend directly.

Anyway, the benefit of this is that it separates the generation of the i.h. from the branching, and enables more flexible style of program, which will become important when we elaborate pattern matching.

[ecavallo]

I too see no reason why it wouldn't work. 👍

[jonsterling]

@ecavallo OK! We can investigate it later. I don't want to get distracted from finishing new-domain.