∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w n : ℕ}
  (_x : (aig : Std.Sat.AIG α) ×' (_ : aig.RefVec n) ×' (_ : ℕ) ×' aig.RefVec w),
  Std.Tactic.BVDecide.BVExpr.bitblast.blastArithShiftRight.go._unary _x =
    PSigma.casesOn _x fun aig distance =>
      PSigma.casesOn distance fun distance curr =>
        PSigma.casesOn curr fun curr acc =>
          if curr < n - 1 then
            let res :=
              Std.Tactic.BVDecide.BVExpr.bitblast.blastArithShiftRight.twoPowShift aig
                { n := n, lhs := acc, rhs := distance, pow := curr + 1 };
            let aig_1 := res.aig;
            have acc_1 := res.vec;
            have this := ⋯;
            have distance := distance.cast this;
            Std.Tactic.BVDecide.BVExpr.bitblast.blastArithShiftRight.go._unary ⟨aig_1, ⟨distance, ⟨curr + 1, acc_1⟩⟩⟩
          else { aig := aig, vec := acc }