rw [← bitblast.go_val_eq_bitblast]
w : Nat
aig : AIG BVBit
expr : BVExpr w
assign : Assignment
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ ⟦{ aig := (bitblast aig expr).aig, ref := (bitblast aig expr).stream.getRef idx✝ hidx✝ }, assign.toAIGAssignment⟧ =
    (eval assign expr).getLsb idx✝
w : Nat
aig : AIG BVBit
expr : BVExpr w
assign : Assignment
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ ⟦{ aig := (bitblast.go aig expr).val.aig, ref := (bitblast.go aig expr).val.stream.getRef idx✝ hidx✝ },
      assign.toAIGAssignment⟧ =
    (eval assign expr).getLsb idx✝