∀ {C : Type u_4} [inst : CategoryTheory.Category.{u_3, u_4} C] (G : CategoryTheory.Functor C TopCat) (X : Type u_2)
  [inst_1 : TopologicalSpace X] (Z B : C) (π : Z ⟶ B) [inst_2 : CategoryTheory.Limits.HasPullback π π]
  (motive :
    ↑{x |
          (ContinuousMap.yonedaPresheaf G X).map (CategoryTheory.Limits.pullback.fst π π).op x =
            (ContinuousMap.yonedaPresheaf G X).map (CategoryTheory.Limits.pullback.snd π π).op x} →
      Prop)
  (x :
    ↑{x |
        (ContinuousMap.yonedaPresheaf G X).map (CategoryTheory.Limits.pullback.fst π π).op x =
          (ContinuousMap.yonedaPresheaf G X).map (CategoryTheory.Limits.pullback.snd π π).op x}),
  (∀ (a : (ContinuousMap.yonedaPresheaf G X).obj (Opposite.op Z))
      (ha :
        a ∈
          {x |
            (ContinuousMap.yonedaPresheaf G X).map (CategoryTheory.Limits.pullback.fst π π).op x =
              (ContinuousMap.yonedaPresheaf G X).map (CategoryTheory.Limits.pullback.snd π π).op x}),
      motive ⟨a, ha⟩) →
    motive x