Chore: Add support for zero-width equalities in the bv_automata tactic

[AtticusKuhn]

Before, the bv_automata tactic would not support theorems of the form:

def alive_1 {w : ℕ} (x x_1 x_2 : BitVec w) : (x_2 &&& x_1 ^^^ x_1) + 1#w + x = x - (x_2 ||| ~~~x_1) := by
  bv_automata

because it did not support the bit-width w = 0.

This PR adds support for the bit-width w = 0 , and the above example has been added as a test case to the test-suite.

As a benefit, the error messages should now be better for bv_automata.

[github-actions[bot]]

Alive Statistics: 67 / 93 (26 failed)

[github-actions[bot]]

Alive Statistics: 67 / 93 (26 failed)

[github-actions[bot]]

Alive Statistics: 67 / 93 (26 failed)

[github-actions[bot]]

Alive Statistics: 67 / 93 (26 failed)