simp [bitblast]
case getLsb
aig : AIG BVBit
assign : BVExpr.Assignment
w✝ : Nat
expr : BVExpr w✝
idx : Nat
⊢ ⟦bitblast aig (getLsb expr idx), assign.toAIGAssignment⟧ = eval assign (getLsb expr idx)
case getLsb
aig : AIG BVBit
assign : BVExpr.Assignment
w✝ : Nat
expr : BVExpr w✝
idx : Nat
⊢ (BVExpr.eval assign expr).getLsb idx = true → idx < w✝