rw [bitblast.go_denote_eq_eval_getLsb]
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✝
no goals