Theorem: BVPred.eval_getLsb (LeanSAT/Reflect/BVExpr/Basic.lean)

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