∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (distance : ℕ)
  (input : aig.RefVec w) (idx : ℕ) (_x : (curr : ℕ) ×' (_ : curr ≤ w) ×' (_ : aig.RefVec curr) ×' idx < curr),
  (Std.Tactic.BVDecide.BVExpr.bitblast.blastRotateLeft.go input distance _x.1 ⋯ _x.2.2.1).get idx ⋯ = _x.2.2.1.get idx ⋯