nat : Type.
0 : nat.
S : nat -> nat.
a : Type.
vec : nat -> Type.
vec' : n : nat -> vec n.
nil : vec 0.
cons : n : nat -> a -> vec n -> vec (S n).