∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (distance : ℕ)
  (input : aig.RefVec w) (_x : (curr : ℕ) ×' (_ : curr ≤ w) ×' aig.RefVec curr),
  aig.decls.size ≤
    (Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftRightConst.go aig input distance _x.1 ⋯ _x.2.2).aig.decls.size