simp [go, blastConst_eq_eval_getLsb]
case const
w : Nat
assign : Assignment
w✝ : Nat
val✝ : BitVec w✝
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
⊢ ⟦{ aig := (go aig (const val✝)).val.aig, ref := (go aig (const val✝)).val.stream.getRef idx hidx },
      assign.toAIGAssignment⟧ =
    (eval assign (const val✝)).getLsb idx
no goals