More informative normalization result type and better conversion check

[ice1000]

Goal being to address the following problems:

1. Conversion is currently lossy (in the future maybe introduce injectivity annotations)
2. Very complex code for handling lossy first-try
3. Redex blocked by meta causing conversion to fail (should delay!)

These can be solved by making whnf return instead of a Term, a disjoint union of the following:

1. an introduction form (represented as a term), so when normalizing an eliminator, we can case on this and do the introduction
2. a neutral form (represented as a term and potentially a variable who blocks the evaluation), so we just stack other things onto it
3. a term with a meta, where the meta being "the reason why I'm blocked"

(maybe 1 and 2 can be combined)

This, together with changes in term comparator, pattern matcher and its compilation, we can solve 1-3. But what remains unclear is how make this compatible with descent.

At this point, changing the definition of descent sounds really bad. Maybe it's time to refactor the core a little bit.