dsimp at hgo
w : Nat
aig : AIG BVBit
a : Nat
assign : Assignment
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx1 : idx < w
hidx2 : curr ≤ idx
res : RefStreamEntry BVBit w
hlt : curr < w
hgo :
  (let res := aig.mkAtomCached (BVBit.mk a ⟨curr, hlt⟩);
    let aig_1 := res.aig;
    let bitRef := res.ref;
    let s := s.cast ⋯;
    let s := s.pushRef bitRef;
    go w aig_1 (curr + 1) s a ⋯) =
    res
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef idx hidx1 }, assign.toAIGAssignment⟧ = (eval assign (var a)).getLsb idx
w : Nat
aig : AIG BVBit
a : Nat
assign : Assignment
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx1 : idx < w
hidx2 : curr ≤ idx
res : RefStreamEntry BVBit w
hlt : curr < w
hgo :
  go w (aig.mkAtomCached (BVBit.mk a ⟨curr, hlt⟩)).aig (curr + 1)
      ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨curr, hlt⟩)).ref) a ⋯ =
    res
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef idx hidx1 }, assign.toAIGAssignment⟧ = (eval assign (var a)).getLsb idx