feat: eliminate sequences of BitVec.ofBool

[tobiasgrosser]

This solves one additional theorems and simplifies a number of theorems we are seeing. We are now at 50/93 solved statements.

[bollu]

It’s a little unclear to me which side this rewrite should be written with for the normal form. As currently written, it attempts to “coalesce” adjacent ofBool bitvectors. I could very well see a case to be made for the opposite direction, where we want to break up bitvectors?

i wonder if we should have a custom simp-set rather than the default simp, then I’d be happy to allow this without a second thought.

[tobiasgrosser]

I am not sure it is worth proactively creating a simp-set here. I would rather add this now and then create a simp-set in case we need the other direction.

[bollu]

I feel uncomfortable merging this in, since it adds simp lemmas to the global simp set. I'm happy with the following solutions:

1. Build a dedicated simp set for alive and use it.
2. Use aesop and see how that fares.

[tobiasgrosser]

@bollu, I created a dedicated simp-set. This reduces the unsolved lemma's to 39.

[bollu]

Thanks!