Next: eliminate thick | Prev: proving checkElim | Up: contents


As you can see, I've done the induction and the computation it unlocked. (Recursion induction gets me the latter for free.) Let's do the base case.

What's blocking the computation is that unevaluated thick application. If only there was a way to split it into constructor cases... There is. thickElim...


Next: eliminate thick | Prev: proving checkElim | Up: contents


Conor's Work Page