∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {old : Std.Sat.AIG α} {w : ℕ}
  (self : Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.BlastUdivOutput old w), old.decls.size ≤ self.aig.decls.size