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

State before:
i w : Nat
e e' : BitVec w
h : e' = e
⊢ e'.getLsb i = e.getLsb i
Tactic:
simp[*]
State after:
no goals