rw [← hgo]
case isTrue
w : Nat
aig : AIG BVBit
a curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
res : RefStreamEntry BVBit w
h✝ : curr < w
hgo :
  go w (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).aig (curr + 1)
      ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).ref) a ⋯ =
    res
⊢ ∀ (hfoo : aig.decls.size ≤ res.aig.decls.size), res.stream.getRef idx ⋯ = (s.getRef idx hidx).cast hfoo
case isTrue
w : Nat
aig : AIG BVBit
a curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
res : RefStreamEntry BVBit w
h✝ : curr < w
hgo :
  go w (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).aig (curr + 1)
      ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).ref) a ⋯ =
    res
⊢ ∀
    (hfoo :
      aig.decls.size ≤
        (go w (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).aig (curr + 1)
                ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).ref) a ⋯).aig.decls.size),
    (go w (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).aig (curr + 1)
              ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).ref) a ⋯).stream.getRef
        idx ⋯ =
      (s.getRef idx hidx).cast hfoo