∀ (aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit) (w a curr : ℕ) (s : aig.RefVec curr) (hcurr : curr ≤ w),
  Std.Tactic.BVDecide.BVExpr.bitblast.blastVar.go aig w a curr s hcurr =
    if hcurr : curr < w then
      let res := aig.mkAtomCached { var := a, w := w, idx := ⟨curr, hcurr⟩ };
      let aig_1 := res.aig;
      have bitRef := res.ref;
      have s := s.cast ⋯;
      have s := s.push bitRef;
      Std.Tactic.BVDecide.BVExpr.bitblast.blastVar.go aig_1 w a (curr + 1) s ⋯
    else
      have hcurr := ⋯;
      { aig := aig, vec := hcurr ▸ s }