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.