∀ (aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit)
  (input : Std.Tactic.BVDecide.BVExpr.WithCache Std.Tactic.BVDecide.BVPred aig),
  ∀ start < aig.decls.size, start < (↑(Std.Tactic.BVDecide.BVPred.bitblast aig input).result).aig.decls.size