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

State before:
assign : Assignment
hi lo a✝ : Nat
expr : BVExpr a✝
⊢ eval assign (extract hi lo expr) = BitVec.extractLsb hi lo (eval assign expr)
Tactic:
rfl
State after:
no goals