Dependent types Mechanization backend

[DCupello1]

This is an experimental branch that does the following:

• Introduces a new pass, "subdep" that combines "sub" and "sub expansion" with the "sub expansion" step made even bigger by expanding relation rules, type cases, and function clauses whenever there is a sub type expression present in a type family's arguments. This allows the validation to be able to reduce these type families and show that they are in fact equivalent.
• Fix on the evaluator that was removing CvtE whenever it failed to convert a numtyp to another.
• Fix on sub pass that did not preserve dependent types correctly in projection functions.
• Fix on improveids in order to aid the evaluator when modifying the environment per definition.

Currently a draft until we figure out testing in this case.

[DCupello1]

@rossberg quick question on this change.

This makes the frontend fail with this issue:

[valid_exp] x
test.spectec:197.30-197.31: validation error: expression's type `val($pppp((3 : nat <:> int), (4 : nat <:> int)))` = `val($pppp(+3, +4))` does not equal expected type `val((7 : nat <:> int))` = `val(+7)`

Which feels like it should not fail since it is able to convert successfully. Do you might know why this would happen?

[rossberg]

Ah, this looks like a sensible bug fix. This causes failure because it was masking another bug, which is that match_exp is missing a case for handling CvtE.

I just pushed a fix.