∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {K : CategoryTheory.Coverage C}
  {motive : (X : C) → (a : CategoryTheory.Sieve X) → K.Saturate X a → Prop} {X : C} {a : CategoryTheory.Sieve X}
  (t : K.Saturate X a),
  (∀ (X : C) (S : CategoryTheory.Presieve X) (hS : S ∈ K.coverings X), motive X (CategoryTheory.Sieve.generate S) ⋯) →
    (∀ (X : C), motive X ⊤ ⋯) →
      (∀ (X : C) (R S : CategoryTheory.Sieve X) (a : K.Saturate X R)
          (a_1 : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → K.Saturate Y (CategoryTheory.Sieve.pullback f S)),
          motive X R a →
            (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (a : R.arrows f), motive Y (CategoryTheory.Sieve.pullback f S) ⋯) → motive X S ⋯) →
        motive X a t