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