Note that Coq will name the constructor `Build_<record name>` for you automatically, even if you don't put it in.