{P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
  {motive : AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P → Sort u_1} →
    (t : AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P) →
      ((exists_preimage_fst_triplet_of_prop :
            ∀ {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} [inst : CategoryTheory.Limits.HasPullback f g],
              P g → ∀ (x : ↥X) (y : ↥Y), f x = g y → ∃ a, (CategoryTheory.Limits.pullback.fst f g) a = x) →
          motive ⋯) →
        motive t