∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] [inst_1 : WellFoundedLT I] (o : Ordinal.{u})
  (g : LocallyConstant ↑(Profinite.NobelingProof.π C fun x => Profinite.NobelingProof.ord I x < o) ℤ) (a : ↑C),
  ((Profinite.NobelingProof.πs C o) g) a =
    g (Profinite.NobelingProof.ProjRestrict C (fun x => Profinite.NobelingProof.ord I x < o) a)