The Vector and Fin libraries are notoriously hard to use, and in some cases even impossible, (try rev (rev x) = x)

See the thread at https://sympa.inria.fr/sympa/arc/coq-club/2017-12/msg00074.html for some discussion.

IMHO, these libraries are a source of pain for many new users and give a bad image of the stdlib, so Coq should provide an alternate mechanism to work with sized lists.