intro idx h1 h2
case isTrue
w : Nat
aig : AIG BVBit
i : Nat
s : aig.RefStream i
a : Nat
hi : i ≤ w
res : AIG.RefStreamEntry BVBit w
h✝ : i < w
hgo :
  go w (aig.mkAtomCached (BVBit.mk a ⟨i, h✝⟩)).aig (i + 1)
      ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨i, h✝⟩)).ref) a ⋯ =
    res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size)
    (h2 :
      idx <
        (go w (aig.mkAtomCached (BVBit.mk a ⟨i, h✝⟩)).aig (i + 1)
                ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨i, h✝⟩)).ref) a ⋯).aig.decls.size),
    (go w (aig.mkAtomCached (BVBit.mk a ⟨i, h✝⟩)).aig (i + 1)
              ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨i, h✝⟩)).ref) a ⋯).aig.decls[idx] =
      aig.decls[idx]
case isTrue
w : Nat
aig : AIG BVBit
i : Nat
s : aig.RefStream i
a : Nat
hi : i ≤ w
res : AIG.RefStreamEntry BVBit w
h✝ : i < w
hgo :
  go w (aig.mkAtomCached (BVBit.mk a ⟨i, h✝⟩)).aig (i + 1)
      ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨i, h✝⟩)).ref) a ⋯ =
    res
idx : Nat
h1 : idx < aig.decls.size
h2 :
  idx <
    (go w (aig.mkAtomCached (BVBit.mk a ⟨i, h✝⟩)).aig (i + 1)
            ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨i, h✝⟩)).ref) a ⋯).aig.decls.size
⊢ (go w (aig.mkAtomCached (BVBit.mk a ⟨i, h✝⟩)).aig (i + 1)
            ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨i, h✝⟩)).ref) a ⋯).aig.decls[idx] =
    aig.decls[idx]