theorem ofBool_1_iff_true {b : Bool} : BitVec.ofBool b = 1#1 ↔ b = true

theorem ofBool_0_iff_false {b : Bool} : BitVec.ofBool b = 0#1 ↔ ¬b = true