Theorem binarySizeMultiple4 : forall b, binarySize (b) mod 4 = 0.
