Support for mutual and nested inductive types at Structural.lean

[leodemoura]

Motivation: examples such as https://github.com/leanprover/lean4/blob/master/tests/lean/run/nestedInductiveRecType.lean
In this example, T is a nested inductive type. So, in the current implementation, any recursive function is defined using well-founded recursion. However, functions defined by well-founded recursion do not have nice definitional equality properties. This is an issue for T.eval. We want the missing definitional equalities when type checking T.default.

[nomeata]

The first half, mutual inductive types, are in #4575. Nested inductive types will follow eventually (hence not closing this yet)

[nomeata]

Forgot to close this with #4733