I am afraid that the only way to simplify is to not use the type “vector”, i.e. a list should not have its length in its type. Just use traditional lists, when you prove something about a length, use the “length” function.