∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (c : BitVec w) (curr : ℕ)
  (hcurr : curr ≤ w) (s : aig.RefVec curr) (idx : ℕ) (hidx : idx < curr) (hfoo : aig.decls.size ≤ aig.decls.size),
  (Std.Tactic.BVDecide.BVExpr.bitblast.blastConst.go aig c curr s hcurr).get idx ⋯ = (s.get idx hidx).cast hfoo