It should be noted though that many top Coq experts recommend to not use dependent vectors. You will likely get along quite a while with a lot of effort but most likely you will have to remove all usage of Vector.t from your project before the end of it. You will save a lot of time if you do this right away. See e.g. this post by Adam Chlipala (author of http://adam.chlipala.net/cpdt/):

https://sympa.inria.fr/sympa/arc/coq-club/2017-12/msg00087.html

or the discussion here:

https://github.com/coq/stdlib/issues/54

The better approach is to use plain lists and proofs that the lists have the size you want.