Theorem: BVDecide.ReifiedBVPred.ofBool_congr (LeanSAT/Reflect/Tactics/BVDecide.lean)

State before:
b : Bool
e' : BitVec 1
h : e' = BitVec.ofBool b
⊢ e'.getLsb 0 = b
Tactic:
cases b <;> simp [h]
State after:
no goals