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

State before:
w : Nat
lhs rhs lhs' rhs' : BitVec w
h1 : lhs' = lhs
h2 : rhs' = rhs
⊢ lhs'.ult rhs' = lhs.ult rhs
Tactic:
simp[*]
State after:
no goals