Binary words

Define a type representing fixed-length sequences of binary values (binary_word: nat->Set) and define the concatenation function for this type.

Remark

Try first do do this exercise without using Coq's library Vectors, then compare your solution with the facilities provided by this library.