fix to bv explanation proofs
fixed let printing for proofs to only letify when term has more than one occurence
fixed bv proof to remove units in analyzeFinal
added regression file for bv proofs
changed signature and code for bv proofs to use dependent BitVec type