Theorem: BVExpr.eval_append (LeanSAT/Reflect/BVExpr/Basic.lean)

State before:
assign : Assignment
a✝¹ : Nat
lhs : BVExpr a✝¹
a✝ : Nat
rhs : BVExpr a✝
⊢ eval assign (lhs.append rhs) = eval assign lhs ++ eval assign rhs
Tactic:
rfl
State after:
no goals