∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] (aig : Std.Sat.AIG α) (w : ℕ) (input : aig.RefVec w)
  (newWidth curr : ℕ) (hcurr : curr ≤ newWidth) (s : aig.RefVec curr) (idx : ℕ) (h1 : idx < aig.decls.size)
  (h2 :
    idx < (Std.Tactic.BVDecide.BVExpr.bitblast.blastZeroExtend.go aig w input newWidth curr hcurr s).aig.decls.size),
  (Std.Tactic.BVDecide.BVExpr.bitblast.blastZeroExtend.go aig w input newWidth curr hcurr s).aig.decls[idx] =
    aig.decls[idx]