1 2 3 4 5
The command has indeed failed with message: => Error: In environment y : nat The term "a y" has type "{y0 : nat | y = y0}" while it is expected to have type "{x : nat | x = y}".