Mutually inductive types

[craff]

Mutually inductive types can be encoded using extra parameters, but this result in a notion of sized type which is not the one we want, and leads to failure of the termination checker.