Gostaria de saber, existe uma biblioteca comumente usada para vetores em coq, ie. listas indexadas pelo tamanho em seu tipo.

Alguns tutoriais fazem referência ao Bvector, mas não é encontrado quando tento importá-lo.

Há Coq.Vectors.Vectordef, mas o tipo definido lá é apenas nomeadot o que me faz pensar que se destina ao uso interno.

Qual é a prática melhor ou mais comum para alguém que não deseja criar sua própria biblioteca? Estou errado sobre os vetores na biblioteca padrão? Ou há outro Lib que estou perdendo? Ou as pessoas simplesmente usam listas, combinadas com provas de seu comprimento?