∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ}
  (_x : (_ : ℕ) ×' (aig : Std.Sat.AIG α) ×' (_ : aig.Ref) ×' (_ : aig.RefVec w) ×' aig.RefVec w) (idx : ℕ)
  (h1 : idx < _x.2.1.decls.size)
  (h2 :
    idx <
      (Std.Tactic.BVDecide.BVExpr.bitblast.mkOverflowBit.go _x.2.1 _x.2.2.2.1 _x.2.2.2.2 _x.1 _x.2.2.1).aig.decls.size),
  (Std.Tactic.BVDecide.BVExpr.bitblast.mkOverflowBit.go _x.2.1 _x.2.2.2.1 _x.2.2.2.2 _x.1 _x.2.2.1).aig.decls[idx] =
    _x.2.1.decls[idx]