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

State before:
assign : Assignment
w idx : Nat
⊢ eval assign (var idx) = BitVec.truncate w (assign.getD idx).bv
Tactic:
rfl
State after:
no goals