Add length to Vect

I thought it would be useful to add the length function to Vect as well.

Motivation:

    indexAsString <- getLine
    let indexAsInt : Integer = cast indexAsString
    let items: Vect _ _ = ["shoe", "bat", "hat"]
    let i = integerToFin indexAsInt $ length items
    maybe (print "invalid index") (\ii => print $ index ii items) i

Is there something I am missing? Some better way to express this without requiring the length function to be defined on Vect.

Also, the implementation is very basic. I tried to figure out a way to express the fact that length is already known through the type and that we should not have to "re-calculate" it but failed.