apply go_le_size
case isTrue.hfoo
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
⊢ (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).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
no goals