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