∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (val : BitVec w)
  (_x : (curr : ℕ) ×' (_ : aig.RefVec curr) ×' curr ≤ w),
  Std.Tactic.BVDecide.BVExpr.bitblast.blastConst.go._unary aig val _x =
    PSigma.casesOn _x fun curr s =>
      PSigma.casesOn s fun s hcurr =>
        if hcurr : curr < w then
          have bitRef := aig.mkConstCached (val.getLsbD curr);
          have s := s.push bitRef;
          Std.Tactic.BVDecide.BVExpr.bitblast.blastConst.go._unary aig val ⟨curr + 1, ⟨s, ⋯⟩⟩
        else
          have hcurr := ⋯;
          hcurr ▸ s