∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (lhsExpr rhsExpr : BitVec w)
  (_x :
    (aig : Std.Sat.AIG α) ×'
      (curr : ℕ) ×'
        (_ : curr ≤ w) ×'
          (cin : aig.Ref) ×'
            (_ : aig.RefVec curr) ×'
              (lhs : aig.RefVec w) ×'
                (rhs : aig.RefVec w) ×'
                  (assign : α → Bool) ×'
                    (_ :
                      ∀ (idx : ℕ) (hidx : idx < w),
                        ⟦assign, { aig := aig, ref := lhs.get idx hidx }⟧ = lhsExpr.getLsbD idx) ×'
                      (_ :
                        ∀ (idx : ℕ) (hidx : idx < w),
                          ⟦assign, { aig := aig, ref := rhs.get idx hidx }⟧ = rhsExpr.getLsbD idx) ×'
                        (_ : ⟦assign, { aig := aig, ref := cin }⟧ = BitVec.carry curr lhsExpr rhsExpr false) ×'
                          (idx : ℕ) ×' (_ : idx < w) ×' curr ≤ idx),
  ⟦_x.2.2.2.2.2.2.2.1,
      {
        aig :=
          (Std.Tactic.BVDecide.BVExpr.bitblast.blastAdd.go _x.1 _x.2.2.2.2.2.1 _x.2.2.2.2.2.2.1 _x.2.1 ⋯ _x.2.2.2.1
              _x.2.2.2.2.1).aig,
        ref :=
          (Std.Tactic.BVDecide.BVExpr.bitblast.blastAdd.go _x.1 _x.2.2.2.2.2.1 _x.2.2.2.2.2.2.1 _x.2.1 ⋯ _x.2.2.2.1
                  _x.2.2.2.2.1).vec.get
            _x.2.2.2.2.2.2.2.2.2.2.2.1 ⋯ }⟧ =
    (⟦_x.2.2.2.2.2.2.2.1, { aig := _x.1, ref := _x.2.2.2.2.2.1.get _x.2.2.2.2.2.2.2.2.2.2.2.1 ⋯ }⟧ ^^
      (⟦_x.2.2.2.2.2.2.2.1, { aig := _x.1, ref := _x.2.2.2.2.2.2.1.get _x.2.2.2.2.2.2.2.2.2.2.2.1 ⋯ }⟧ ^^
        BitVec.carry _x.2.2.2.2.2.2.2.2.2.2.2.1 lhsExpr rhsExpr false))