Definition build_vector {A: Set} (n: nat) := build_vector_aux n O (@nil A).