fact: Fixpoint binary_word_concat (n:nat)(w1:binary_word n)(m:nat)(w2:binary_word m) {struct w1} : binary_word (n+m) := match w1 in binary_word p return binary_word (p+m) with bw0 => w2 | bwS q b w1' => bwS (q+m) b (binary_word_concat q w1' m w2) end.