∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (distance : ℕ)
  (input : aig.RefVec w) (assign : α → Bool) (curr : ℕ) (hcurr : curr ≤ w) (s : aig.RefVec curr) (idx : ℕ)
  (hidx1 : idx < w),
  curr ≤ idx →
    ⟦assign,
        { aig := aig,
          ref :=
            (Std.Tactic.BVDecide.BVExpr.bitblast.blastArithShiftRightConst.go input distance curr hcurr s).get idx
              hidx1 }⟧ =
      if hidx : distance + idx < w then ⟦assign, { aig := aig, ref := input.get (distance + idx) hidx }⟧
      else ⟦assign, { aig := aig, ref := input.get (w - 1) ⋯ }⟧