∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w n : ℕ} (aig : Std.Sat.AIG α) (distance : aig.RefVec n)
  (curr : ℕ) (acc : aig.RefVec w),
  curr < n - 1 →
    ∀
      (this :
        aig.decls.size ≤
          (Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftRight.twoPowShift aig
                  { n := n, lhs := acc, rhs := distance, pow := curr + 1 }).aig.decls.size),
      InvImage (fun x1 x2 => x1 < x2)
        (fun x =>
          PSigma.casesOn x fun aig distance =>
            PSigma.casesOn distance fun distance curr => PSigma.casesOn curr fun curr acc => n - 1 - curr)
        ⟨(Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftRight.twoPowShift aig
              { n := n, lhs := acc, rhs := distance, pow := curr + 1 }).aig,
          ⟨distance.cast this,
            ⟨curr + 1,
              (Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftRight.twoPowShift aig
                  { n := n, lhs := acc, rhs := distance, pow := curr + 1 }).vec⟩⟩⟩
        ⟨aig, ⟨distance, ⟨curr, acc⟩⟩⟩