∀ {I : Type u} (C C_1 : Set (I → Bool)),
  C = C_1 →
    ∀ [inst : LinearOrder I] [inst_1 : WellFoundedLT I] {o o_1 : Ordinal.{u}} (e_o : o = o_1)
      (ho : o < Ordinal.type fun x1 x2 => x1 < x2) (a a_1 : I → Bool),
      a = a_1 → Profinite.NobelingProof.C1 C ho a = Profinite.NobelingProof.C1 C_1 ⋯ a_1