This directory contains the lemmas used for the normalizing simp set of bv_decide.
They are a combination of:
rules that turn hypotheses involving BitVec and Bool into something of the form x = true
where x only consists of BitVec and Bool terms, notably no Prop. This makes it easy to
reflect the terms.