apply blastVar.go_eq_eval_getLsb
w : Nat
aig : AIG BVBit
var : BVVar w
assign : Assignment
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ ⟦{ aig := (blastVar aig var).aig, ref := (blastVar aig var).stream.getRef idx✝ hidx✝ }, assign.toAIGAssignment⟧ =
    (eval assign (BVExpr.var var.ident)).getLsb idx✝
case a
w : Nat
aig : AIG BVBit
var : BVVar w
assign : Assignment
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ 0 ≤ idx✝