{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.Precoverage C} →
      {motive : J.IsStableUnderSup → Sort u_1} →
        (t : J.IsStableUnderSup) →
          ((sup_mem_coverings :
                ∀ {X : C} {R S : CategoryTheory.Presieve X},
                  R ∈ J.coverings X → S ∈ J.coverings X → R ⊔ S ∈ J.coverings X) →
              motive ⋯) →
            motive t