(semi-deprecated) Basic theorems about the "default" behavior of
bit-vector operations when their inputs are ill-formed (e.g., not integers, not
naturals).
We tend not to include this any more, because it should mostly be
subsumed by the nat-equiv and int-equiv congruence reasoning.
