∀ {w : ℕ} (aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit) (a curr : ℕ) (hcurr : curr ≤ w) (s : aig.RefVec curr) (idx : ℕ)
  (hidx : idx < curr),
  (Std.Tactic.BVDecide.BVExpr.bitblast.blastVar.go aig w a curr s hcurr).vec.get idx ⋯ = (s.get idx hidx).cast ⋯