∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α)
  (target : Std.Tactic.BVDecide.BVExpr.bitblast.TwoPowShiftTarget aig w) (lhs : BitVec w) (rhs : BitVec target.n)
  (assign : α → Bool),
  (∀ (idx : ℕ) (hidx : idx < w), ⟦assign, { aig := aig, ref := target.lhs.get idx hidx }⟧ = lhs.getLsbD idx) →
    (∀ (idx : ℕ) (hidx : idx < target.n), ⟦assign, { aig := aig, ref := target.rhs.get idx hidx }⟧ = rhs.getLsbD idx) →
      ∀ (idx : ℕ) (hidx : idx < w),
        ⟦assign,
            { aig := (Std.Tactic.BVDecide.BVExpr.bitblast.blastArithShiftRight.twoPowShift aig target).aig,
              ref :=
                (Std.Tactic.BVDecide.BVExpr.bitblast.blastArithShiftRight.twoPowShift aig target).vec.get idx hidx }⟧ =
          (lhs.sshiftRight' (rhs &&& BitVec.twoPow target.n target.pow)).getLsbD idx