nat : Type.

x : nat.

y : x.