Using the type binary_word defined in
this file
as follows, define
a function binary_word_or that computes the bit-wise or operation
between two words of the same length (like the | operator in the C
language).
Prove that binary_word_or is idempotent.