Definition binarySizePadded16 (b : binaryExp) : nat :=
  asMultipleOf16 (binarySize b).
