∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] (l : Profinite.NobelingProof.Products I),
  Profinite.NobelingProof.Products.isGood C l =
    (Profinite.NobelingProof.Products.eval C l ∉
      Submodule.span ℤ (Profinite.NobelingProof.Products.eval C '' {m | m < l}))