Theorem: BVDecide.ReifiedBVExpr.append_congr (LeanSAT/Reflect/Tactics/BVDecide.lean)

State before:
lw rw : Nat
lhs lhs' : BitVec lw
rhs rhs' : BitVec rw
h1 : lhs' = lhs
h2 : rhs' = rhs
⊢ lhs' ++ rhs' = lhs ++ rhs
Tactic:
simp[*]
State after:
no goals