Comment by bojo

    app : Vect n a -> Vect m a -> Vect (n + m) a

That is pretty amazing if you ask me. I look forward to the day when we all use languages which save programmers from themselves.