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

State before:
assign : Assignment
v a✝ : Nat
expr : BVExpr a✝
⊢ eval assign (zeroExtend v expr) = BitVec.zeroExtend v (eval assign expr)
Tactic:
rfl
State after:
no goals