∀ {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S}
  (motive : (T : AlgebraicGeometry.Scheme.Pullback.Triplet f g) × ↥(AlgebraicGeometry.Spec T.tensor) → Prop)
  (h : (T : AlgebraicGeometry.Scheme.Pullback.Triplet f g) × ↥(AlgebraicGeometry.Spec T.tensor)),
  (∀ (T : AlgebraicGeometry.Scheme.Pullback.Triplet f g) (p : ↥(AlgebraicGeometry.Spec T.tensor)), motive ⟨T, p⟩) →
    motive h