Definition build_list {A: Set} := build_list_aux (@nil A).