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